Concurrent C Minor project
Concurrent C Minor is an
international research
project to connect machine-verified source programs in sequential and
concurrent programming languages to machine-verified optimizing compilers.
It takes inspiration from
Xavier Leroy's
design of the (sequential) C Minor language and verified compiler
and has goals complementary to Leroy's
CompCert project.
Work in progress
- Sequential C Minor small-step operational semantics,
soundness proof of sequential Separation Logic (Appel, Blazy)
- Coq tactics for separation logic (Appel, Zappa Nardelli)
- Concurrent C Minor operational semantics,
pseudosequential semantics, soundness proof of
Concurrent Separation Logic (Appel, Hobor, Zappa Nardelli)
- Redesign of Concurrent Separation Logic (Appel, O'Hearn)
- Verified translation of Featherweight Java to C minor (Compagnoni, Appel)
Affiliated researchers
(people who give us good advice...)
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.
Tactics for Separation Logic,
by Andrew W. Appel, January 2006.
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.
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.
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.
Funding
This research is supported by Princeton University, INRIA,
the National Science Foundation (CCF-0540914).
Last major overhaul of this page: December 2006.
