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.
Document type :
Conference papers
Liste complète des métadonnées

Cited literature [25 references]  Display  Hide  Download

https://hal.inria.fr/hal-00790310
Contributor : Claude Marché <>
Submitted on : Tuesday, February 19, 2013 - 5:45:40 PM
Last modification on : Monday, September 3, 2018 - 12:40:01 PM
Document(s) archivé(s) le : Monday, May 20, 2013 - 4:05:12 AM

File

main.pdf
Files produced by the author(s)

Identifiers

  • 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. ⟨hal-00790310⟩

Share

Metrics

Record views

860

Files downloads

460