Let's Verify This with Why3

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

doi:10.1007/s10009-014-0314-5

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.

Document type :

Journal articles

Software Tools for Technology Transfer (STTT), Springer, 2015, 17 (6), pp.709-727. 〈10.1007/s10009-014-0314-5〉

Domain :

Computer Science [cs] / Logic in Computer Science [cs.LO]

Liste complète des métadonnées

https://hal.inria.fr/hal-00967132
Contributor : Claude Marché <>
Submitted on : Friday, March 28, 2014 - 9:22:17 AM
Last modification on : Thursday, February 7, 2019 - 2:24:39 PM
Document(s) archivé(s) le : Saturday, June 28, 2014 - 11:00:42 AM

main.pdf

Files produced by the author(s)

Let's Verify This with Why3

File

Identifiers

Collections

Citation

Export

Metrics

1720

1095

Contact

Let's Verify This with Why3

File

Identifiers

Collections

Citation

Export

Share

Metrics

1720

1095

Contact