The WMC project is funded by JCJC
2011, a program of the Agence Nationale de
The WMC project investigates the formal verification of realistic
compilers for concurrent dialects of the mainstram languages C and
C++. It targets both the x86 and Power/ARM architectures, which
require radically different compilation strategies and proof methods.
In addition it studies the design and correctness proofs of novel
compile-time optimisations for these languages and compilers.
The Technical Annex to the
contract illustrates the initial objectives of the project.