FramaC
What is FramaC ?
FramaC is a suite of tools dedicated to the analysis of the source code of so are written in C.
FramaC gathers several static analysis techniques in a single collaborative framework. The collaborative approach of FramaC allows static analyzers to build upon the results already computed by other analyzers in the framework. Thanks to this approach, FramaC provides sophisticated tools, such as a slicer and dependency analysis.
Static analysis ?
Static analysis of source code is the science of computing synthetic information about the source code without executing it.
To most programmers, static analysis means measuring the source code with respect to various metrics (examples are the number of comments per line of code and the depth of nested control structures). This kind of syntactic analysis can be implemented in FramaC but it is not the focus of the project.
Others may be familiar with heuristic bugfinding tools. These tools take more of an indepth look at the source code and try to pinpoint dangerous constructions and likely bugs (locations in the code where an error might happen at runtime). These heuristic tools do not find all such bugs, and sometimes they alert the user for constructions which are in fact not bugs.
FramaC is closer to these heuristic tools than it is to software metrics tools, but it has two important differences with them: it aims at being correct, that is, never to remain silent for a location in the source code where an error can happen at runtime. And it allows its user to manipulate functional specifications, and to prove that the source code satisfies these specifications.
You may now want to go on to the description of FramaC's features, to a page with more details about its modular, extensible architecture, or you may want to see FramaC in action on an example.
PILAT
What is PILAT ?
PILAT (for Polynomial Invariants by Linear Algebra Tool) is an invariant generator based on the study of matrices. It processes loops with polynomial assignments and linearize them, then searches for left eigenvectors of the resulting matrix. Those vectors expresses invariants of the loop.
Pilat is a plugin of the FramaC framework. It is written in Ocaml and it is open source under LGPL licence, you can find it here. If you use OPAM, you can get the latest version with "opam install pilat". We applied our tool to this benchmark on deterministic loops and on nondeterministic loops.
Related publications

De Oliveira Steven, Bensalem Saddek and Prevosto Virgile(2017, October)
Synthesizing invariants by solving solvable loops

De Oliveira Steven, Bensalem Saddek and Prevosto Virgile (2016, October)
Polynomial invariants by linear algebra

De Oliveira Steven, Bensalem Saddek and Prevosto Virgile (2016, June)
Algèbre lineaire pour invariant polynomiaux (slides)
CaFE
What is CaFE ?
CaFE (for Caret Framac's Extension) is a modelchecker being developped in the FramaC framework. It is based on the temporal logic CaRet, a temporal logic based on Call and Return properties.
CaFE uses the results of Value , a powerful static analyser in FramaC, in order to generate a recursive state machine over which it performs a modelchecking procedure. It is not open source, but it is described in this french article.
Presentation of CaFE with Pilat at the FramaC days 2016 : poster.