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

Displayed time zone: Saskatchewan, Central America change

10:30 - 11:35
Program verificationCPP at Maurepas
Chair(s): Nikhil Swamy Microsoft Research
10:30
21m
Talk
A Verified Packrat Parser Interpreter for Parsing Expression Grammars
CPP
Clement Blaudeau Ecole Polytechnique, Natarajan Shankar SRI International, USA
DOI Pre-print Media Attached
10:51
22m
Talk
Proof Pearl: Braun Trees
CPP
Tobias Nipkow Technische Universität München, Thomas Sewell Chalmers University of Technology, Sweden
DOI Pre-print Media Attached
11:13
22m
Talk
FreeSpec: Specifying, Verifying and Executing Impure Computations in Coq
CPP
Thomas Letan ANSSI, Yann Régis-Gianas IRIF, University Paris Diderot and CNRS, France / INRIA PI.R2
DOI Pre-print Media Attached