Weak Memory Concurrency

Home Publications Software

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.

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

Last update: