Skip to Main content Skip to Navigation
Conference papers

FreeSpec: Specifying, Verifying and Executing Impure Computations in Coq

Thomas Letan 1 Yann Régis-Gianas 2
2 PI.R2 - Design, study and implementation of languages for proofs and programs
CNRS - Centre National de la Recherche Scientifique, Inria de Paris, UP - Université de Paris, IRIF (UMR_8243) - Institut de Recherche en Informatique Fondamentale
Abstract : FreeSpec is a framework for the Coq theorem prover whichallows for specifying and verifying complex systems as hierarchies of components verified both in isolation and incomposition. While FreeSpec was originally introduced forreasoning about hardware architectures, in this article wepropose a novel iteration of FreeSpec formalism specificallydesigned to write certified programs and libraries. Then, wepresent in depth how we use this formalism to verify a staticfiles webserver. We use this opportunity to present Free-Spec proof automation tactics, and to demonstrate how theysuccessfully erase FreeSpec internal definitions to let usersfocus on the core of their proofs. Finally, we introduce Free-Spec.Exec, a plugin for Coq to seamlessly execute certifiedprograms written with FreeSpec.
Document type :
Conference papers
Complete list of metadata

Cited literature [38 references]  Display  Hide  Download
Contributor : Thomas Letan Connect in order to contact the contributor
Submitted on : Saturday, December 21, 2019 - 11:43:19 AM
Last modification on : Wednesday, November 3, 2021 - 6:40:46 AM
Long-term archiving on: : Sunday, March 22, 2020 - 1:11:37 PM


Files produced by the author(s)




Thomas Letan, Yann Régis-Gianas. FreeSpec: Specifying, Verifying and Executing Impure Computations in Coq. CPP 2020 - 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2020, Nouvelle-Orléans, United States. pp.1-15, ⟨10.1145/3372885.3373812⟩. ⟨hal-02422273⟩



Record views


Files downloads