Skip to Main content Skip to Navigation
Journal articles

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 - Formally Verified Programs, Certified Tools and Numerical Computations
LRI - Laboratoire de Recherche en Informatique, Inria Saclay - Ile de France
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
Complete list of metadatas
https://hal.inria.fr/hal-00967132
Contributor : Claude Marché <>
Submitted on : Friday, March 28, 2014 - 9:22:17 AM
Last modification on : Tuesday, December 8, 2020 - 9:42:29 AM
Long-term archiving on: : Saturday, June 28, 2014 - 11:00:42 AM

File

Vignette du document
main.pdf
Files produced by the author(s)

Identifiers

Collections

CNRS | CEA | UMR8623 | LRI-VALS | INRIA | DRT | CEA-UPSAY | CENTRALESUPELEC | 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⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

2193

Files downloads

1804

 

Contact                    Legal Notice                    Personal Data