Conference proceeding
Fast and flexible proof checking for SMT
Proceedings of the 7th International Workshop on satisfiability modulo theories, pp.6-13
SMT '09
08/02/2009
DOI: 10.1145/1670412.1670414
Abstract
Fast and flexible proof checking can be implemented for SMT using the Edinburgh Logical Framework with Side Conditions (LFSC). LFSC provides a declarative format for describing proof systems as signatures. We describe several optimizations for LFSC proof checking, and report experiments on QF_IDL benchmarks showing proof-checking overhead of 32% of the solving time required by our clsat solver.
Details
- Title: Subtitle
- Fast and flexible proof checking for SMT
- Creators
- Duckki Oe - University of IowaAndrew Reynolds - University of IowaAaron Stump - University of Iowa
- Resource Type
- Conference proceeding
- Publication Details
- Proceedings of the 7th International Workshop on satisfiability modulo theories, pp.6-13
- Series
- SMT '09
- DOI
- 10.1145/1670412.1670414
- Publisher
- ACM
- Grant note
- DOI: 10.13039/100000143, name: Division of Computing and Communication Foundations, award: CCF-0841554
- Language
- English
- Date published
- 08/02/2009
- Academic Unit
- Computer Science
- Record Identifier
- 9984259431502771
Metrics
9 Record Views