The Verified Software Toolchain (VST) is a tool for specifying and verifying functional correctness properties of C programs in the Coq proof assistant with a machine-checked semantic model that connects assertions to the operational semantics of CompCert's Clight language. Specifications in VST's program logic, Verifiable C, are expressed in higher-order concurrent separation logic, an extension of the classical verification calculi by Floyd and Hoare that modularly supports almost all language features of C.
The talk will motivate key design decisions using case studies from cryptographic libraries and other industry-strength code bases. Time permitting, I will also discuss modularity aspects of CompCert itself and efforts to connect VST to verified operating system kernels and other components of a typical system stack, as presently carried out in the NSF expedition "The Science of Deep Specification."
Lennart Beringer is a research scholar at Princeton University, where he has been been a member of the VST project since 2009 and presently serves as the associate director the the NSF Expedition "The Science of Deep Specification." His interests span the fields of programming languages, verification and applied security, with a focus on the application of interactive proof assistants. Having earned his Ph.D. from the University of Edinburgh in 2002, his previous work includes the development of proof-carrying-code architectures for resource consumption and information flow security, and the use of relational reasoning principles for verifying effective program transformations.
For more information, please contact David Naumann [email protected]