Anwendungsorientierte Formale Verifikation

Der Lehrstuhl für Anwendungsorientierte formale Verifikation, geleitet von Prof. Bernhard Beckert, existiert seit 2009 am Institut für Theoretische Informatik und der KIT-Fakultät für Informatik.

Unser Forschungsgebiet is die praktische Anwendung von Logik und Formalen Methoden für die Spezifikation und Verifikation von Software. Insbesondere beschäftigen wir uns mit den folgenden Anwendungsgebieten:

  • Verifikation von funktionalen Eigenschaften und Software-Verlässlichkeit
  • Verifikation von relationalen Eigenschaften und Software-Evolution
  • Verifikation von Informationsfluss-Eigenschaften und IT-Sicherheit
  • Verifikation von Social-Choice-Algorithmen und Wahlverfahren

Neuigkeiten

Neues KeY-Buch veröffentlicht

Das neue KeY-Buch beschreibt alle Aspekte der Deduktiven Softwareverifikation, wie sie im KeY-Ansatz realisiert ist. Dieses Buch ist die umfassende Informationsquelle für das KeY-Werkzeug Version 2.x.

Das KeY-Buch ist erhältlich beim Springer-Verlag als Band 10001 in LNCS und bei Springer Link.

Mehr Informationen

Kontakt
Institut für Theoretische Informatik

Am Fasanengarten 5
76131 Karlsruhe
Deutschland
Tel.: +49 721 608-44023
Fax: +49 721 608-44021
E-Mail: simone.meinhartHfu8∂kit.edu

Anreise