Expressiveness + automation + soundness: Towards combining SMT solvers and interactive proof assistants

Pascal Fontaine*, Jean Yves Marion, Stephan Merz, Leonor Prensa Nieto, Alwen Tiu

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

54 Citations (Scopus)

Abstract

Formal system development needs expressive specification languages, but also calls for highly automated tools. These two goals are not easy to reconcile, especially if one also aims at high assurances for correctness. In this paper, we describe a combination of Isabelle/HOL with a proof-producing SMT (Satisfiability Modulo Theories) solver that contains a SAT engine and a decision procedure for quanti fier-free first-order logic with equality. As a result, a user benefits from the expressiveness of Isabelle/HOL when modeling a system, but obtains much better automation for those fragments of the proofs that fall within the scope of the (automatic) SMT solver. Soundness is not compromised because all proofs are submitted to the trusted kernel of Isabelle for certification. This architecture is straightforward to extend for other interactive proof assistants and proof-producing reasoners.

Original languageEnglish
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems - 12th International Conference, TACAS 2006. Held as Part of the Joint European Conf. on Theory and Practice of Software, ETAPS 2006
Pages167-181
Number of pages15
DOIs
Publication statusPublished - 2006
Externally publishedYes
Event12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2006. Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006 - Vienna, Austria
Duration: 25 Mar 20062 Apr 2006

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume3920 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2006. Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006
Country/TerritoryAustria
CityVienna
Period25/03/062/04/06

Fingerprint

Dive into the research topics of 'Expressiveness + automation + soundness: Towards combining SMT solvers and interactive proof assistants'. Together they form a unique fingerprint.

Cite this