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 - 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

Domain :

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

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 : Thursday, October 3, 2019 - 2:04:03 PM
Long-term archiving on : 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

1905

1267

Contact

Let's Verify This with Why3

File

Identifiers

Collections

Citation

Export

Share

Metrics

1905

1267

Contact