Let's Verify This with Why3

François Bobot; Jean-Christophe Filliâtre; Claude Marché; Andrei Paskevich

Let's Verify This with Why3

François Bobot ¹ 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

Domaine :

Informatique [cs] / Logique en informatique [cs.LO]

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 : jeudi 5 avril 2018 - 12:30:22
Document(s) archivé(s) le : samedi 28 juin 2014 - 11:00:42

main.pdf

Fichiers produits par l'(les) auteur(s)

Let's Verify This with Why3

Fichier

Identifiants

Collections

Citation

Exporter

Métriques

1449

834

Contact

Let's Verify This with Why3

Fichier

Identifiants

Collections

Citation

Exporter

Partager

Métriques

1449

834

Contact