Skip to Main content Skip to Navigation
Conference papers

Satisfiability Modulo Bounded Checking

Simon Cruanes 1, 2
1 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
MPII - Max-Planck-Institut für Informatik, Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
2 MOSEL - Proof-oriented development of computer-based systems
LORIA - FM - Department of Formal Methods
Abstract : We describe a new approach to find models for a computational higher-order logic with datatypes. The goal is to find counterexamples for conjectures stated in proof assistants. The technique builds on narrowing [14] but relies on a tight integration with a SAT solver to analyze conflicts precisely, eliminate sets of choices that lead to failures, and sometimes prove unsatisfiability. The architecture is reminiscent of that of an SMT solver. We present the rules of the calculus, an implementation, and some promising experimental results.
Document type :
Conference papers
Complete list of metadata

Cited literature [18 references]  Display  Hide  Download

https://hal.inria.fr/hal-01572531
Contributor : Simon Cruanes Connect in order to contact the contributor
Submitted on : Tuesday, August 8, 2017 - 4:08:43 PM
Last modification on : Wednesday, November 3, 2021 - 7:57:37 AM

File

paper.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Simon Cruanes. Satisfiability Modulo Bounded Checking. International Conference on Automated Deduction (CADE), Leonardo de Moura, Aug 2017, Gothenburg, Sweden. pp.114-129, ⟨10.1007/978-3-319-63046-5_8⟩. ⟨hal-01572531⟩

Share

Metrics

Les métriques sont temporairement indisponibles