Write a Blog >>
Mon 20 Jan 2020 11:13 - 11:35 at Maurepas - Program verification Chair(s): Nikhil Swamy

FreeSpec is a framework for the Coq theorem prover which allows for implementing, specifying and verifying complex systems as hierarchies of components verified both in isolation and in composition. FreeSpec was originally designed for reasoning about hardware architectures. In this article, we present a new iteration on the FreeSpec formalism we call Mutual Obligations logic specifically designed to develop certified programs and libraries. Then, we present how we use this formalism to verify a webserver for static files. We use this opportunity to present FreeSpec proof automation tactics, and demonstrate how they successfully erase FreeSpec internal definitions to let users focus on the core goals of their proofs. Finally, we introduce FreeSpec.Exec, a plugin for Coq to seamlessly execute certified programs written with FreeSpec.

Mon 20 Jan

CPP-2020-papers
10:30 - 11:35: CPP 2020 - Program verification at Maurepas
Chair(s): Nikhil SwamyMicrosoft Research
CPP-2020-papers10:30 - 10:51
Talk
Clement BlaudeauEcole Polytechnique, Natarajan ShankarSRI International, USA
DOI Pre-print Media Attached
CPP-2020-papers10:51 - 11:13
Talk
Tobias NipkowTechnische Universität München, Thomas SewellChalmers University of Technology, Sweden
DOI Pre-print Media Attached
CPP-2020-papers11:13 - 11:35
Talk
Thomas LetanANSSI, Yann Régis-GianasIRIF, University Paris Diderot and CNRS, France / INRIA PI.R2
DOI Pre-print Media Attached