One Logic To Use Them All

Jean-Christophe Filliâtre 1, 2
1 TOCCATA - Certified Programs, Certified Tools, Certified Floating-Point Computations
LRI - Laboratoire de Recherche en Informatique, UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8623
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.
Type de document :
Communication dans un congrès
Maria Paola Bonacina. CADE 24 - the 24th International Conference on Automated Deduction, Jun 2013, Lake Placid, NY, United States. Springer, 2013
Liste complète des métadonnées


https://hal.inria.fr/hal-00809651
Contributeur : Jean-Christophe Filliâtre <>
Soumis le : mardi 9 avril 2013 - 16:15:33
Dernière modification le : jeudi 9 février 2017 - 15:57:23
Document(s) archivé(s) le : lundi 3 avril 2017 - 02:58:53

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00809651, version 1

Citation

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

Partager

Métriques

Consultations de
la notice

976

Téléchargements du document

575