Frama-C verifier

Frama-C verifier
[Google Scholar] [Website] [Wikipedia]

Notes: undefined behaviour
Papers: cuoq:sefm:2012

Frama-C (the Framework for Modular Analysis of C programs) is a set of interoperable program analyzers for C programs. It is structured as a plugin architecture supporting value analysis, deductive verification, weakest precondition calculation, impact analysis and program slicing. This is supported by a framework based on the CIL frontend to parse C code, and some common analyses and libraries.

Frama-C also forms the basis of the tis interpreter that executes C programs and detects undefined behaviour.

Frama-C has commercial support from TrustInSoft.

Undefined behaviour

  • A case study on formal verification of the Anaxagoros hypervisor paging system with Frama-C [blanchard:fmics:2015]
  • Frama-C: A software analysis perspective [cuoq:sefm:2012]
  • Formal verification of a memory allocation module of Contiki with Frama-C: a case study [mangano:crisis:2016]
  • überSpark: Enforcing verifiable object abstractions for automated compositional security analysis of a hypervisor [vasudevan:usenix:2016]