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.

Conference Day
Mon 20 Jan

Displayed time zone: Saskatchewan, Central America change

10:30 - 11:35
Program verificationCPP at Maurepas
Chair(s): Nikhil SwamyMicrosoft Research
10:30
21m
Talk
A Verified Packrat Parser Interpreter for Parsing Expression Grammars
CPP
Clement BlaudeauEcole Polytechnique, Natarajan ShankarSRI International, USA
DOI Pre-print Media Attached
10:51
22m
Talk
Proof Pearl: Braun Trees
CPP
Tobias NipkowTechnische Universität München, Thomas SewellChalmers University of Technology, Sweden
DOI Pre-print Media Attached
11:13
22m
Talk
FreeSpec: Specifying, Verifying and Executing Impure Computations in Coq
CPP
Thomas LetanANSSI, Yann Régis-GianasIRIF, University Paris Diderot and CNRS, France / INRIA PI.R2
DOI Pre-print Media Attached