Software
OCaml
From a language standpoint, OCaml extends the core Caml language with a full-fledged object and class layer, as well as a powerful module system, all joined together by a sound, polymorphic type system featuring type inference. The OCaml system is an industrial-strength implementation of this language, featuring a high-performance native-code compiler for several processor architectures (x86-32 bits, x86-64 bits, PowerPC, ARM, etc.), as well as a bytecode compiler and an interactive loop for quick development and portability. The OCaml distribution includes a standard library and a number of programming tools: a replay debugger, lexer and parser generators, a documentation generator, etc.
The CompCert C verified compiler
The CompCert verified compiler is a compiler for a large subset of the C programming language that generates code for the PowerPC processor. The distinguishing feature of CompCert is that it has been formally verified using the Coq proof assistant: the generated assembly code is formally guaranteed to behave as prescribed by the semantics of the source C code. By ruling out the possibility of compiler-introduced bugs, verified compilers strengthen the guarantees that can be obtained by applying formal methods to critical embedded programs.
The diy tool suite
The diy suite provides a set of tools for testing shared memory models: the litmus tool for running tests on hardware, various generators for producing tests from concise specifications, and herd, a memory model simulator. Tests are small programs written in the C language, in x86, Power or ARM assembler that can thus be generated from concise specifications, run on hardware, or simulated on top of memory models. Memory models are written in the domain-specific language cat. Test results can be handled and compared using additional tools.