Since no single technique will ever be able to fit all software verification needs, Frama-C aims at combining program analysis technics, provided as plug-ins, to guarantee the absence of bugs in C programs.
An analysis framework fueled by formal methods
The main particularity of Frama-C is that it embeds tools based on formal methods, that are mathematical technics to reason about programs. Thus, most of the analyzers in Frama-C are sound: they never remain silent when a bug might happen.
Absence of runtime errors and beyond
Undefined behaviors in C programs can cause safety and security issues. Many tools can be used to find these runtime errors, but most of them provide heuristic bug finding that can miss bugs, whereas Frama-C is meant to guarantee that no bug can happen. Moreover, Frama-C provides a formal specification language, ACSL, which gives the opportunity not only to prove that no runtime error can happen, but also conformance to a functional specification.
Widely used, from experimental research to industry
Frama-C is largely used for teaching, experimental research, and industrial applications. It has been used successfully for certification purposes for DO-178, IEC 60880, Common Criteria EAL 6-7 … You may now want to go on to the description of Frama-C’s features or to a page with more details about its modular, extensible architecture