TY - GEN
T1 - Verified software toolchain (Invited talk)
AU - Appel, Andrew W.
PY - 2011
Y1 - 2011
N2 - The software toolchain includes static analyzers to check assertions about programs; optimizing compilers to translate programs to machine language; operating systems and libraries to supply context for programs. Our Verified Software Toolchain verifies 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, on a weakly-consistent-shared-memory machine. Our verification approach is modular, in that proofs about operating systems or concurrency libraries are oblivious of the programming language or machine language, proofs about compilers are oblivious of the program logic used to verify static analyzers, and so on. The approach is scalable, in that each component is verified in the semantic idiom most natural for that component. Finally, the verification is foundational: the trusted base for proofs of observable properties of the machine-language program includes only the operational semantics of the machine language, not the source language, the compiler, the program logic, or any other part of the toolchain-even when these proofs are carried out by source-level static analyzers. In this paper I explain some semantic techniques for building a verified toolchain.
AB - The software toolchain includes static analyzers to check assertions about programs; optimizing compilers to translate programs to machine language; operating systems and libraries to supply context for programs. Our Verified Software Toolchain verifies 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, on a weakly-consistent-shared-memory machine. Our verification approach is modular, in that proofs about operating systems or concurrency libraries are oblivious of the programming language or machine language, proofs about compilers are oblivious of the program logic used to verify static analyzers, and so on. The approach is scalable, in that each component is verified in the semantic idiom most natural for that component. Finally, the verification is foundational: the trusted base for proofs of observable properties of the machine-language program includes only the operational semantics of the machine language, not the source language, the compiler, the program logic, or any other part of the toolchain-even when these proofs are carried out by source-level static analyzers. In this paper I explain some semantic techniques for building a verified toolchain.
UR - http://www.scopus.com/inward/record.url?scp=79953220810&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=79953220810&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-19718-5_1
DO - 10.1007/978-3-642-19718-5_1
M3 - Conference contribution
AN - SCOPUS:79953220810
SN - 9783642197178
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 1
EP - 17
BT - Programming Languages and Systems - 20th European Symposium on Programming, ESOP 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Proceedings
T2 - 20th European Symposium on Programming, ESOP 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011
Y2 - 26 March 2011 through 3 April 2011
ER -