|
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 Verified Software Toolchain
project assures with machine-checked proofs
that the assertions claimed at the top of the toolchain really hold in
the machine-language program, running in the operating-system context.
This research paper
gives an overview of the project.
Early research leading to the Verified Software Toolchain
was conducted in the Concurrent C minor project.
|
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
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.
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.
Funding
Parts of this research are funded by:
- 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.
