Let's Verify This with Why3 (original) (raw)

Loading...

Article Dans Une Revue International Journal on Software Tools for Technology Transfer Année : 2015

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
2 TOCCATA - Formally Verified Programs, Certified Tools and Numerical Computations
3 LRI - Laboratoire de Recherche en Informatique

François Bobot

LSL - Laboratoire Sûreté des Logiciels

Jean-Christophe Filliâtre

TOCCATA - Formally Verified Programs, Certified Tools and Numerical Computations

LRI - Laboratoire de Recherche en Informatique

Claude Marché

TOCCATA - Formally Verified Programs, Certified Tools and Numerical Computations

LRI - Laboratoire de Recherche en Informatique

CV

Andrei Paskevich

TOCCATA - Formally Verified Programs, Certified Tools and Numerical Computations

LRI - Laboratoire de Recherche en Informatique

CV

Résumé

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.

Domaines

Fichier principal

Vignette du fichier

main.pdf (360.25 Ko) Télécharger le fichier

Origine Fichiers produits par l'(les) auteur(s)
Licence Autorisation HAL

Connectez-vous pour contacter le contributeur

https://inria.hal.science/hal-00967132

Soumis le : vendredi 28 mars 2014-09:22:17

Dernière modification le : mercredi 26 février 2025-15:22:03

Archivage à long terme le : samedi 28 juin 2014-11:00:42

Télécharger pour visualiser

Dates et versions

hal-00967132 , version 1 (28-03-2014)

Licence

Autorisation HAL

Identifiants

Citer

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

Exporter

Collections

2522 Consultations

3273 Téléchargements

Altmetric

Partager