Programmverifikation mit Frama-C, Vampire und Aligator

01.02.2010 - 31.12.2011

Auftragsforschungsprojekt

We study challenging benchmark examples of Dassault Aviation, with the purpose of improving a uniform and automated framework for program verification within the FRAMA-C toolchain of Dassault. To this end, we develop the first-order theorem prover Vampire to handle various theories, design an SMT-TPTP parser, and improve the invariant generator package ALIGATOR to generate valid loop assertions over unbounded data structures.

Personen

Projektleiter_in

Univ.Prof.in Dr.in techn. Laura Kovacs MSc (E185)

Institut

E185 - Institut für Computersprachen

Auftrag/Kooperation

Dassault Aviation, France

Forschungsschwerpunkte

Information and Communication Technology

Schlagwörter

Deutsch	Englisch
Program Verifikation	Program Verification
Theorem Beweis	Theorem Proving
Invariant	Invariant Generation
Interpolation	Interpolation

Externe Partner_innen

University of Manchester
ETH Zürich