Program Verification with Frama-C, Vampire and Aligator

01.02.2010 - 31.12.2011
Assigned research project
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.

People

Project leader

Institute

Contract/collaboration

  • Dassault Aviation, France

Research focus

  • Computational Intelligence: 100%

Keywords

GermanEnglish
Program VerifikationProgram Verification
Theorem BeweisTheorem Proving
InvariantInvariant Generation
InterpolationInterpolation

External partner

  • University of Manchester
  • ETH Zürich

Publications