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
Times are displayed in time zone: (GMT-06:00) Saskatchewan, Central America change

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