Concurrent C Minor project

The Concurrent C Minor project (2006-2010) is now one component of the Verified Software Toolchain.

We develop program logics (such as Concurrent Separation Logic) that have machine-checked proofs of soundness w.r.t. the C Minor operational semantics; this connects to the correctness proof of the CompCert compiler.

There are applications to embedded systems (for C programs) and to high-assurance high-level programming (via machined-verified translators from high-level languages to C).

Participants

Andrew W. Appel
Princeton University

Lennart Beringer
Princeton University

Robert Dockins
Princeton University

Aquinas Hobor
National U. of Singapore

Gordon Stewart
Princeton University

Collaborators and affiliated researchers

Xavier Leroy
INRIA

John Hatcliff
Kansas State U.

Sandrine Blazy
IRISA & U. Rennes I

Francesco Zappa Nardelli
INRIA

Rationale

In some application domains it is not enough to build reliable software systems, one wants proved-correct software. This is the case for safety-critical systems (where software bugs can cause injury or death) and for security-critical applications (where an attacker is deliberately searching for, and exploiting, software bugs). Since proofs are large and complex, the proof-checking must be mechanized. Machine-checked proofs of real software systems are difficult, but now should be possible, given the recent advances in the theory and engineering of mechanized proof systems applied to software verification. But there are several challenges:

Real software systems are usually built from components in different programming languages.
Some parts of the program need full correctness proofs, which must be constructed with great effort; other parts need only safety proofs, which can be constructed automatically.
One reasons about correctness at the source-code level, but one runs a machine-code program translated by a compiler; the compiler must be proved correct.
These proofs about different properties, with respect to different programming languages, must be integrated together end-to-end in a way that is also proved correct and machine-checked.

We address these challenges by defining a high-level intermediate language, Concurrent C Minor (CCm), with a small-step operational semantics representable in machine-checked proof assistants (we use Coq). We define a Concurrent Separation Logic for reasoning directly about source programs written in CCm. In addition, CCm is suitable as a target language for compilers from Java, C, C#, ML, and other languages. This will allow safe and well-specified interaction of program modules written in different programming languages. Finally, CCm is a concurrent language with a threads-and-locks model similar to Cthreads.

Publications

Foundational High-level Static Analysis, by Andrew W. Appel. In CAV 2008 Workshop on Exploiting Concurrency Efficiently and Correctly, July 2008.

Relational program logics in decomposed style, by Lennart Beringer, July 2010.

Formal Verification of Coalescing Graph-Coloring Register Allocation, by Sandrine Blazy, Benoit Robillard, and Andrew W. Appel. In ESOP 2010: 19th European Symposium on Programming, March 2010.

A Theory of Indirection via Approximation, by Aquinas Hobor, Robert Dockins, and Andrew W. Appel. In POPL 2010: The 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, January 2010.

A Fresh Look at Separation Algebras and Share Accounting by Robert Dockins, Aquinas Hobor, and Andrew W. Appel. To appear in Seventh Asian Symposium on Programming Languages and Systems (APLAS 2009), December 2009.

Multimodal Separation Logic for Reasoning About Operational Semantics, by Robert Dockins, Andrew W. Appel, and Aquinas Hobor, (to appear) in Twenty-fourth Conference on the Mathematical Foundations of Programming Semantics, May 2008.

Automating Separation Logic for Concurrent C Minor, by William Mansky. Undergraduate thesis, May 2008.

Oracle Semantics for Concurrent Separation Logic by Aquinas Hobor, Andrew W. Appel, and Francesco Zappa Nardelli. European Symposium on Programming (ESOP), April 2008. Extended version with appendix.

Separation Logic for Small-step C Minor, by Andrew W. Appel and Sandrine Blazy. in TPHOLs 2007: 20th International Conference on Theorem Proving in Higher-Order Logics, September 2007. Tactics for Separation Logic, by Andrew W. Appel, January 2006.

Funding

Parts of this research are funded by:

Air Force Office of Scientific Research (via subcontract to Kansas State University), Evidence-based trust in large-scale MLS systems.
National Science Foundation, Combining Foundational and Lightweight Formal Methods to Build Certifiably Dependable Software.

This research has also been supported by Princeton University, INRIA, and National Science Foundation Grant CCF-0540914.

Last overhaul of this page: June 2009.