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 Appel
Andrew W. Appel

Princeton University
Lennart Beringer
Lennart Beringer

Princeton University
Robert Dockins
Robert Dockins

Princeton University
Aquinas Hobor
Aquinas Hobor

National U. of Singapore
Gordon Stewart
Gordon Stewart

Princeton University

Collaborators and affiliated researchers

Xavier Leroy
Xavier Leroy

INRIA
John Hatcliff
John Hatcliff

Kansas State U.
Sandrine Blazy
Sandrine Blazy

IRISA & U. Rennes I
Francesco Zappa Nardelli
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: 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:

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

Last overhaul of this page: June 2009.