Qed. Computing what remains to be proved - CEA - Commissariat à l’énergie atomique et aux énergies alternatives Accéder directement au contenu
Communication Dans Un Congrès Année : 2014

Qed. Computing what remains to be proved

Résumé

We propose a framework for manipulating in a efficient way terms and formulæ in classical logic modulo theories. Qed was initially designed for the generation of proof obligations of a weakest-precondition engine for C programs inside the Frama-C framework, but it has been implemented as an independent library. Key features of Qed include on-the-fly strong normalization with various theories and maximal sharing of terms in memory. Qed is also equipped with an extensible simplification engine. We illustrate the power of our framework by the implementation of non-trivial simplifications inside the Wp plug-in of Frama-C. These optimizations have been used to prove industrial, critical embedded softwares.
Fichier principal
Vignette du fichier
qed.pdf (509.52 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

cea-01809013 , version 1 (08-04-2021)

Identifiants

Citer

Loïc Correnson. Qed. Computing what remains to be proved. NFM 2014 - NASA Formal Methods, 6th International Symposium, Apr 2014, Houston, United States. pp.215-229, ⟨10.1007/978-3-319-06200-6_17⟩. ⟨cea-01809013⟩
156 Consultations
213 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More