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.
Notes related to Frama-C verifier
Papers related to Frama-C verifier
- 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]