Application-oriented Formal Verification

The research group on Application-oriented Formal Verification led by Prof. Bernhard Beckert exists since 2009 at the Institute of Theoretical Informatics and the KIT Department of Informatics.

Our main research topic is the practical application of logic and formal methods for the specification and verification of software. In particular, we address the following application areas:

  • verification of functional properties and software dependability
  • verification of relational properties and software evolution
  • verification of information-flow properties and IT security
  • verification of social choice algorithms and voting schemes


The new KeY Book is available

The new book covers deductive software verification as realised by the KeY approach. It constitutes the ultimate source for the KeY tool since version 2.x.

The KeY book is published by Springer as vol. 10001 in the LNCS series) and available at Springer Link.

More information

CVE-2016-6313: Critical bug found in PRNG (August 2016)

CVE-2016-6313 - Critical bug in the GnuPG/Libgcrypt PRNG found with the help of the Entroposcope tool, developed by Felix Dörre and Dr. Vladimir Klebanov as part of the DeduSec project within the RS³ priority programme. The paper describing how Entroposcope works was presented at ACM CCS 2016 in Vienna in October 2016.

Update: Presentation at the 33th Chaos Communication Congress (33C3)

Institute of Theoretical Informatics

Am Fasanengarten 5
76131 Karlsruhe
Phone: +49 721 608-44023
Fax:    +49 721 608-44021
Email: simone.meinhartHfu8∂