Verified Software Toolchain
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.
Abstraction and Subsumption in Modular Verification of C Programs, by Lennart Beringer and Andrew W. Appel. FM2019: 23rd International Symposium on Formal Methods, October 2019.
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. (Local copy)
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.
