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
LIST - Laboratoire d'Intégration des Systèmes et des Technologies : DRT/LIST
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
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
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 : Friday, February 17, 2017 - 4:10:25 PM
Document(s) archivé(s) le : Saturday, June 28, 2014 - 11:00:42 AM

File

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00967132, version 1

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. <hal-00967132>

Share

Metrics

Record views

1082

Document downloads

580