Journal article
SMT proof checking using a logical framework
FORMAL METHODS IN SYSTEM DESIGN, Vol.42(1), pp.91-118
02/01/2013
DOI: 10.1007/s10703-012-0163-3
Abstract
Producing and checking proofs from SMT solvers is currently the most feasible method for achieving high confidence in the correctness of solver results. The diversity of solvers and relative complexity of SMT over, say, SAT means that flexibility, as well as performance, is a critical characteristic of a proof-checking solution for SMT. This paper describes such a solution, based on a Logical Framework with Side Conditions (LFSC). We describe the framework and show how it can be applied for flexible proof production and checking for two different SMT solvers, clsat and cvc3. We also report empirical results showing good performance relative to solver execution time.
Details
- Title: Subtitle
- SMT proof checking using a logical framework
- Creators
- Aaron Stump - University of IowaDuckki Oe - University of IowaAndrew Reynolds - University of IowaLiana Hadarean - New York UniversityCesare Tinelli - University of Iowa
- Resource Type
- Journal article
- Publication Details
- FORMAL METHODS IN SYSTEM DESIGN, Vol.42(1), pp.91-118
- Publisher
- Springer Nature
- DOI
- 10.1007/s10703-012-0163-3
- ISSN
- 0925-9856
- eISSN
- 1572-9893
- Number of pages
- 28
- Grant note
- 0914877; 0914956 / US National Science Foundation; National Science Foundation (NSF)
- Language
- English
- Date published
- 02/01/2013
- Academic Unit
- Computer Science
- Record Identifier
- 9984259479002771
Metrics
4 Record Views