Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants

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

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 quantifier-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.

© Springer-Verlag 2006

Available as: PDF

Reference

@InProceedings{fontaine:automation,
  author = 	 {Pascal Fontaine and Jean-Yves Marion and Stephan Merz
                  and Leonor Prensa Nieto and Alwen Tiu},
  title = 	 {Expressiveness + Automation + Soundness: Towards
                  Combining {SMT} Solvers and Interactive Proof Assistants},
  booktitle = {12th Intl. Conf. Tools and Algorithms for the Construction
                  and Analysis of Systems (TACAS 2006)},
  pages = 	 {167--181},
  year = 	 2006,
  editor = 	 {Holger Hermanns and Jens Palsberg},
  volume = 	 3920,
  series = 	 {Lecture Notes in Computer Science},
  address = 	 {Vienna, Austria},
  publisher = {Springer-Verlag}
}