FreeSpec: Specifying, Verifying and Executing Impure Computations in Coq - Archive ouverte HAL Access content directly
Conference Papers Year :

FreeSpec: Specifying, Verifying and Executing Impure Computations in Coq

(1) , (2)
1
2

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.
Fichier principal
Vignette du fichier
article.pdf (509.29 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-02422273 , version 1 (21-12-2019)

Identifiers

Cite

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⟩
509 View
1049 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More