Why3 -- Where Programs Meet Provers

Jean-Christophe Filliâtre 1, 2 Andrei Paskevich 1, 2
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 Why3, a tool for deductive program verification, and WhyML, its programming and specification language. WhyML is a first-order language with polymorphic types, pattern matching, and inductive predicates. Programs can make use of record types with mutable fields, type invariants, and ghost code. Verification conditions are discharged by Why3 with the help of various exist- ing automated and interactive theorem provers. To keep verification conditions tractable and comprehensible, WhyML imposes a static control of aliases that ob- viates the use of a memory model. A user can write WhyML programs directly and get correct-by-construction OCaml programs via an automated extraction mech- anism. WhyML is also used as an intermediate language for the verification of C, Java, or Ada programs. We demonstrate the benefits of Why3 and WhyML on non- trivial examples of program verification.
Type de document :
Communication dans un congrès
ESOP'13 22nd European Symposium on Programming, Mar 2013, Rome, Italy. Springer, 7792, 2013, LNCS; Proceedings of the 22nd European Symposium on Programming}
Liste complète des métadonnées


https://hal.inria.fr/hal-00789533
Contributeur : Jean-Christophe Filliâtre <>
Soumis le : lundi 18 février 2013 - 14:09:31
Dernière modification le : jeudi 9 février 2017 - 15:56:41
Document(s) archivé(s) le : dimanche 19 mai 2013 - 04:03:21

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00789533, version 1

Citation

Jean-Christophe Filliâtre, Andrei Paskevich. Why3 -- Where Programs Meet Provers. ESOP'13 22nd European Symposium on Programming, Mar 2013, Rome, Italy. Springer, 7792, 2013, LNCS; Proceedings of the 22nd European Symposium on Programming}. <hal-00789533>

Partager

Métriques

Consultations de
la notice

1462

Téléchargements du document

1084