The software toolchain includes static analyzers to check assertions
Alumni, collaborators, and affiliated researchers
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
- 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
Verifiable C, a program logic for the
C programming language.
Verifiable C is proved sound with respect to the
operational semantics of CompCert C;
in turn, the CompCert verified optimizing C compiler is
proved correct with respect to the assembly-language
semantics of the PowerPC, ARM, and x86 processors.
Abstraction and Subsumption in Modular Verification of C Programs,
by Lennart Beringer and Andrew W. Appel.
FM2019: 23rd International Symposium on Formal Methods,
VST-Floyd: A separation logic tool to verify
correctness of C programs,
by Qinxiang Cao, Lennart Beringer, Samuel Gruetter, Josiah Dodds, and Andrew W. Appel. Journal of Automated Reasoning 61(1), pp. 367-422, 2018.
A verified messaging system,
by William Mansky, Andrew W. Appel, and Aleksey Nogin.
OOPSLA’17: ACM Conference on Object-Oriented Programming Systems, Languages, and Applications, October 2017. Proceedings of the ACM on Programming Languages (PACM/PL) volume 1, issue OOPSLA, paper 87, 2017.
Bringing order to the separation logic jungle, by Qinxiang Cao, Santiago Cuellar, and Andrew W. Appel.
APLAS’17: 15th Asian Symposium on Programming Languages and Systems, November 2017.
Modular Verification for Computer Security, by Andrew W. Appel. In
CSF 2016: 29th IEEE Computer Security Foundations Symposium, June 2016.
Verified Correctness and Security of OpenSSL HMAC,
by Lennart Beringer, Adam Petcher, Katherine Q. Ye, and Andrew W. Appel.
In 24th USENIX Security Symposium, pages 207-221, August 2015.
by Gordon Stewart, Lennart Beringer, Santiago Cuellar, and Andrew W. Appel.
POPL 2015: The 42nd Annual ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages, pages 275-287, January 2015.
Second Edition: Verification of a Cryptographic Primitive: SHA-256.
This is a very minor revision (as explained in its abstract) of
Verification of a Cryptographic Primitive: SHA-256, by Andrew W. Appel,
ACM Transactions on Programming Languages and Systems
37(2) 7:1-7:31, April 2015.
Verified Correctness and Security of mbedTLS HMAC-DRBG
by Katherine Q. Ye, Matthew Green, Naphat Sanguansin, Lennart Beringer, Adam Petcher, and Andrew W. Appel.
CCS’17: ACM Conference on Computer and Communications Security,
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.
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),
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.
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,
Tactics for Separation Logic,
by Andrew W. Appel, January 2006.
Parts of this research are funded by:
- Defense Advanced Research Projects Agency,
Compositionality and Automation for Robotics Security.
- 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.
Early research leading to the Verified Software Toolchain
was conducted in the Concurrent C minor project.
Last overhaul of this page: April 2013