The software toolchain includes static analyzers to check assertions
about your program; optimizing compilers to translate your program to
machine language; operating systems and libraries to supply context
for your program. The |

## Research resultsVerifiable C tools:Book, software, documentation Download Technical overview of the VST logic
Mechanized Software Library VeriStar certified entailment checker VeriSmall foundationally verified shape analysis |
(e-book) (hardcover) |

Andrew W. Appel Princeton University |
Lennart Beringer Princeton University |
Gordon Stewart Princeton University |
Josiah Dodds Princeton University |
Qinxiang Cao Princeton University |
Santiago Cuellar Princeton University |

Xavier Leroy INRIA |
Robert Dockins Portland State U. |
Aquinas Hobor National U. Singapore |
Sandrine Blazy IRISA & U. Rennes I |

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

Verified Compilation for Shared-memory C,
by Lennart Beringer, Gordon Stewart, Robert Dockins, and Andrew W. Appel.
*23rd European Symposium on Programming (ESOP'14),*
April 2014.

*Program Logics for Certified Compilers*,
by Andrew W. Appel with Robert Dockins, Aquinas Hobor, Lennart Beringer, Josiah Dodds, Gordon Stewart, Sandrine Blazy, and Xavier Leroy.
Cambridge University Press, 2014.

Mostly Sound Type System Improves a Foundational
Program Verifier, by Josiah Dodds and Andrew W. Appel.
*3rd International Conference on Certified Programs and Proofs (CPP 2013),*
December 2013.

*Verifiable C: Applying the Verified Software Toolchain to C programs*,
by Andrew W. Appel. 2013.

Verified Heap Theorem Prover by Paramodulation, by Gordon Stewart, Lennart Beringer, and Andrew W. Appel.
In *ICFP 2012: The 17th ACM SIGPLAN International Conference on Functional Programming*, September 2012.

Operational Refinement for Compiler Correctness by Robert Dockins. PhD thesis, Princeton University, September 2012.

A Certificate Infrastructure for Machine-Checked Proofs of Conditional Information Flow, by Torben Amtoft, Josiah Dodds, Zhi Zhang, Andrew Appel, Lennart Beringer, John Hatcliff, Xinming Ou and Andrew Cousino.
*First Conference on Principles of Security and Trust (POST 2012)*,
March 2012.

VeriSmall: Verified Smallfoot Shape Analysis,
by Andrew W. Appel.
In *CPP 2011: First International Conference on
Certified Programs and Proofs,* December 2011.

Relational Decomposition, by Lennart Beringer.
*Proceedings of the Second International Conference on Interactive
Theorem Proving (ITP 2011),* pages 39-54, August 2011. Springer LNCS 6898.

Verified Software Toolchain, by Andrew W. Appel.
In *ESOP 2011: 20th European Symposium on Programming,*
LNCS 6602, pp. 1-17, March 2011.

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.

Local Actions for a Curry-style Operational Semantics by Gordon Stewart and Andrew W. Appel.
In *PLPV'11: 5th ACM SIGPLAN Workshop on Programming Languages meets Program Verification*, January 29, 2011.

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.

Foundational High-level Static Analysis,
by Andrew W. Appel. In *CAV 2008 Workshop on Exploiting Concurrency
Efficiently and Correctly*, July 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.

- Defense Advanced Research Projects Agency,
*Compositionality and Automation for Robotics Security*. - Air Force Office of Scientific Research,
*Evidence-based trust in large-scale MLS systems*. - National Science Foundation,
*Combining Foundational and Lightweight Formal Methods to Build Certifiably Dependable Software.*

Early research leading to the Verified Software Toolchain
was conducted in the *Concurrent C minor* project.

Last overhaul of this page: April 2013