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).

Andrew W. Appel Princeton University |
Lennart Beringer Princeton University |
Robert Dockins Princeton University |
Aquinas Hobor National U. of Singapore |
Gordon Stewart Princeton University |

Xavier Leroy INRIA |
John Hatcliff Kansas State U. |
Sandrine Blazy IRISA & U. Rennes I |
Francesco Zappa Nardelli INRIA |

- 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.

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.

- 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.