Skip to Main content Skip to Navigation
New interface
Conference papers

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
Complete list of metadata

Cited literature [25 references]  Display  Hide  Download
Contributor : Claude Marché Connect in order to contact the contributor
Submitted on : Tuesday, February 19, 2013 - 5:45:40 PM
Last modification on : Sunday, June 26, 2022 - 11:58:19 AM
Long-term archiving on: : Monday, May 20, 2013 - 4:05:12 AM


Files produced by the author(s)


  • HAL Id : hal-00790310, version 1



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⟩



Record views


Files downloads