Skip to Main content Skip to Navigation
New interface
Conference papers

One Logic To Use Them All

Abstract : Deductive program verification is making fast progress these days. One of the reasons is a tremendous improvement of theorem provers in the last two decades. This includes various kinds of automated theorem provers, such as ATP systems and SMT solvers, and interactive proof assistants. Yet most tools for program verification are built around a single theorem prover. Instead, we defend the idea that a collaborative use of several provers is a key to easier and faster verification. This paper introduces a logic that is designed to target a wide set of theorem provers. It is an extension of first-order logic with polymorphism, algebraic data types, recursive definitions, and inductive predicates. It is implemented in the tool Why3, and has been successfully used in the verification of many non-trivial programs.
Document type :
Conference papers
Complete list of metadata

Cited literature [37 references]  Display  Hide  Download
Contributor : Jean-Christophe Filliâtre Connect in order to contact the contributor
Submitted on : Tuesday, April 9, 2013 - 4:15:33 PM
Last modification on : Sunday, June 26, 2022 - 11:58:32 AM
Long-term archiving on: : Monday, April 3, 2017 - 2:58:53 AM


Files produced by the author(s)


  • HAL Id : hal-00809651, version 1



Jean-Christophe Filliâtre. One Logic To Use Them All. CADE 24 - the 24th International Conference on Automated Deduction, Jun 2013, Lake Placid, NY, United States. ⟨hal-00809651⟩



Record views


Files downloads