Verified Software Toolchain: a powerful and practical tool
The Verified Software Toolchain is a tool for machine-checked proofs of correctness of C programs, with respect to specifications in separation logic and functional models in Coq. During the DeepSpec project (2015-2020) we have enhanced its program logic (Verifiable C) and its proof automation tools with better support for C control flow, concurrent shared-memory threads, more sophisticated separation-logic reasoning techniques, encapsulation of global variables, efficiency of separation-logic proof script execution, support for 64-bit or 32-bit C, many usability improvements, data abstraction, and strong support for modular proofs of modular programs. I will describe and illustrate some of these features.
Mon 15 JunDisplayed time zone: Pacific Time (US & Canada) change
09:00 - 11:00
| Cerberus: executable reference semantics and memory object models for ISO and de facto C
|Verified Software Toolchain: a powerful and practical tool
Andrew W. Appel Princeton