Skip to Main content Skip to Navigation
Conference papers

A Nelson-Oppen based Proof System using Theory Specific Proof Systems

Frédéric Besson 1 Pierre-Emmanuel Cornilleau 1 David Pichardie 1
1 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : SMT solvers are nowadays pervasive in verification tools. When the verification is about a critical system, the result of the SMT solver is also critical and cannot be trusted. The SMT-LIB 2.0 is a standard interface for SMT solvers but does not specify the output of the get-proof command. We present a proof system that is geared towards SMT solvers and follows their conceptually modular architecture. Our proof system makes a clear distinction between propositional and theory reasoning. Moreover, individual theories provide specific proof systems that are combined using the Nelson-Oppen proof scheme. We propose specific proof systems for linear real arithmetic (LRA) and uninterpreted functions (EUF) and discuss proof generation and proof checking. We have evaluated the cost of generating proofs in our proof system. Our experiments on benchmarks taken from the SMT-LIB library show that the simple mechanisms used in our approach suffice for a large majority of the selected benchmarks.
Document type :
Conference papers
Complete list of metadatas

Cited literature [19 references]  Display  Hide  Download
Contributor : Pascal Fontaine <>
Submitted on : Wednesday, March 7, 2012 - 3:17:40 PM
Last modification on : Friday, July 10, 2020 - 4:00:15 PM
Long-term archiving on: : Friday, November 23, 2012 - 4:01:07 PM


Explicit agreement for this submission


  • HAL Id : hal-00677193, version 1


Frédéric Besson, Pierre-Emmanuel Cornilleau, David Pichardie. A Nelson-Oppen based Proof System using Theory Specific Proof Systems. First International Workshop on Proof eXchange for Theorem Proving - PxTP 2011, Aug 2011, Wrocław, Poland. ⟨hal-00677193⟩



Record views


Files downloads