Frama-C gathers several static analysis techniques in a single collaborative framework. The collaborative approach of Frama-C allows static analyzers to build upon the results already computed by other analyzers in the framework. Thanks to this approach, Frama-C provides sophisticated tools, such as a slicer and dependency analysis.
Frama-C allows to verify that the source code complies with a provided formal specification. Functional specifications can be written in a dedicated language, ACSL. The specifications can be partial, concentrating on one aspect of the analyzed program at a time.
Also see the Frama-C home page.