One Logic to Use Them All

Deductive program verication 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 verication 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 verication. This paper introduces a logic that is designed to target a wide set of theorem provers. It is an extension of rst-order logic with polymorphism, algebraic data types, recursive denitions, and inductive predicates. It is implemented in the tool Why3, and has been successfully used in the verication of many non-trivial programs.

• Type: Journal
• Year: 2013
• Where: CADE
• Authors: Jean-Christophe Filliâtre
• Keywords: CADE 2013, Logical Reasoning