HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

Why3 -- Where Programs Meet Provers

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.
Document type :
Conference papers
Complete list of metadata

Cited literature [6 references]  Display  Hide  Download

Contributor : Jean-Christophe Filliâtre Connect in order to contact the contributor
Submitted on : Monday, February 18, 2013 - 2:09:31 PM
Last modification on : Tuesday, November 16, 2021 - 11:45:00 AM
Long-term archiving on: : Sunday, May 19, 2013 - 4:03:21 AM


Files produced by the author(s)


  • HAL Id : hal-00789533, version 1


Jean-Christophe Filliâtre, Andrei Paskevich. Why3 -- Where Programs Meet Provers. ESOP'13 22nd European Symposium on Programming, Mar 2013, Rome, Italy. ⟨hal-00789533⟩



Record views


Files downloads