The WMC project is funded by JCJC 2011, a program of the Agence Nationale de la Recherche.

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.

• Francesco Zappa Nardelli, INRIA (main investigator)
• Luc Maranget, INRIA
• Peter Sewell, U. of Cambridge
• Viktor Vafeiadis, MPI-SWS

The Technical Annex to the contract illustrates the initial objectives of the project.