Skip to Main content Skip to Navigation
Conference papers

FreeSpec: Specifying, Verifying and Executing Impure Computations in Coq

Thomas Letan 1, 2 Yann Régis-Gianas 3
2 CIDRE - Confidentialité, Intégrité, Disponibilité et Répartition
CentraleSupélec, Inria Rennes – Bretagne Atlantique , IRISA-D1 - SYSTÈMES LARGE ÉCHELLE
3 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 metadatas

Cited literature [38 references]  Display  Hide  Download

https://hal.inria.fr/hal-02422273
Contributor : Thomas Letan <>
Submitted on : Saturday, December 21, 2019 - 11:43:19 AM
Last modification on : Friday, July 10, 2020 - 4:01:26 PM
Long-term archiving on: : Sunday, March 22, 2020 - 1:11:37 PM

File

article.pdf
Files produced by the author(s)

Identifiers

Citation

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⟩

Share

Metrics

Record views

626

Files downloads

1980