Xavier Leroy – Communications of the ACM

Research and Advances Dec 1 2011

Software misbehaves all too often. This is a truism, but also the driving force behind many computing techniques intended to increase software reliability, safety, and security, ranging from basic testing to full formal verification.

Computing Applications

Author Archives

Research and Advances Jul 1 2009

Formal Verification of a Realistic Compiler

This paper reports on the development and formal verification of CompCert, a compiler from Clight (a large subset of the C programming language) to PowerPC assembly code, using the Coq proof assistant both for programming the compiler and for proving its correctness.

Computing Applications

Shape the Future of Computing

ACM encourages its members to take a direct hand in shaping the future of the association. There are more ways than ever to get involved.

Get Involved