Constraint solving for finite model finding in SMT solvers
From MaRDI portal
Publication:4593094
DOI10.1017/S1471068417000175zbMath1379.68286arXiv1706.00096OpenAlexW2963499262MaRDI QIDQ4593094
Andrew Reynolds, Clark Barrett, Cesare Tinelli
Publication date: 9 November 2017
Published in: Theory and Practice of Logic Programming (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1706.00096
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Computer aided verification. 25th international conference, CAV 2013, Saint Petersburg, Russia, July 13--19, 2013. Proceedings
- Computing finite models by reduction to function-free clause logic
- Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis
- Solving quantified verification conditions using satisfiability modulo theories
- Isabelle/HOL. A proof assistant for higher-order logic
- Automated deduction -- CADE-24. 24th international conference on automated deduction, Lake Placid, NY, USA, June 9--14, 2013. Proceedings
- Being careful about theory combination
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
- Finding Finite Models in Multi-sorted First-Order Logic
- Finite Quantification in Hierarchic Theorem Proving
- Solving SAT and SAT Modulo Theories
- Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL
- iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
- Simplify: a theorem prover for program checking
- Efficient E-Matching for SMT Solvers
- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
- Extending Sledgehammer with SMT Solvers
- Exploiting Symmetry in SMT Problems
- Splitting on Demand in SAT Modulo Theories
- On Local Reasoning in Verification
- Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder
- Kodkod: A Relational Model Finder
