Why3: Shepherd Your Herd of Provers

François Bobot 1, 2 Jean-Christophe Filliâtre 1, 2 Claude Marché 1, 2 Andrei Paskevich 1, 2
2 PROVAL - Proof of Programs
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR
Abstract : Why3 is the next generation of the Why software verification platform. Why3 clearly separates the purely logical specification part from generation of verification conditions for programs. This article focuses on the former part. Why3 comes with a new enhanced language of logical specification. It features a rich library of proof task transformations that can be chained to produce a suitable input for a large set of theorem provers, including SMT solvers, TPTP provers, as well as interactive proof assistants.
Type de document :
Communication dans un congrès
Boogie 2011: First International Workshop on Intermediate Verification Languages, 2011, Wroclaw, Poland. pp.53-64, 2011
Liste complète des métadonnées

Littérature citée [25 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00790310
Contributeur : Claude Marché <>
Soumis le : mardi 19 février 2013 - 17:45:40
Dernière modification le : vendredi 10 novembre 2017 - 14:52:02
Document(s) archivé(s) le : lundi 20 mai 2013 - 04:05:12

Fichier

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

Identifiants

  • HAL Id : hal-00790310, version 1

Collections

Citation

François Bobot, Jean-Christophe Filliâtre, Claude Marché, Andrei Paskevich. Why3: Shepherd Your Herd of Provers. Boogie 2011: First International Workshop on Intermediate Verification Languages, 2011, Wroclaw, Poland. pp.53-64, 2011. 〈hal-00790310〉

Partager

Métriques

Consultations de
la notice

579

Téléchargements du document

328