Let's Verify This with Why3

François Bobot 1 Jean-Christophe Filliâtre 2, 3 Claude Marché 2, 3 Andrei Paskevich 2, 3
1 LSL - Laboratoire Sûreté des Logiciels
DILS - Département Ingénierie Logiciels et Systèmes : DRT/LIST/DILS
2 TOCCATA - Certified Programs, Certified Tools, Certified Floating-Point Computations
LRI - Laboratoire de Recherche en Informatique, UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8623
3 LRI - Laboratoire de Recherche en Informatique
Abstract : We present solutions to the three challenges of the VerifyThis competition held at the 18th FM symposium in August 2012. These solutions use the Why3 environment for deductive program verification.
Type de document :
Article dans une revue
Software Tools for Technology Transfer (STTT), Springer, 2015, 17 (6), pp.709-727. 〈10.1007/s10009-014-0314-5〉
Liste complète des métadonnées
https://hal.inria.fr/hal-00967132
Contributeur : Claude Marché <>
Soumis le : vendredi 28 mars 2014 - 09:22:17
Dernière modification le : lundi 30 juillet 2018 - 10:36:39
Document(s) archivé(s) le : samedi 28 juin 2014 - 11:00:42

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

CEA | UMR8623 | LRI-VALS | INRIA | DRT | CEA-UPSAY | CENTRALESUPELEC | UNIV-PARIS-SACLAY | LIST

Citation

François Bobot, Jean-Christophe Filliâtre, Claude Marché, Andrei Paskevich. Let's Verify This with Why3. Software Tools for Technology Transfer (STTT), Springer, 2015, 17 (6), pp.709-727. 〈10.1007/s10009-014-0314-5〉. 〈hal-00967132〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

1518

Téléchargements de fichiers

881

Contact


archive-ouverte@inria.fr