Parallelizing SMT solving: lazy decomposition and conciliation
From MaRDI portal
Publication:1749390
DOI10.1016/j.artint.2018.01.001zbMath1444.68169OpenAlexW2791364807MaRDI QIDQ1749390
Publication date: 16 May 2018
Published in: Artificial Intelligence (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.artint.2018.01.001
parallelizationsatisfiability modulo theoriesconciliationlazy decompositiontheory of equality with uninterpreted functions
Parallel algorithms in computer science (68W10) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)
Related Items (1)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- An interpolating sequent calculus for quantifier-free Presburger arithmetic
- Constraint solving for interpolation
- Tools and algorithms for the construction and analysis of systems. 15th international conference, TACAS 2009, held as part of the joint European conferences on theory and practice of software, ETAPS 2009, York, UK, March 22--29, 2009. Proceedings
- Computer aided verification. 21st international conference, CAV 2009, Grenoble, France, June 26--July 2, 2009. Proceedings
- Automated reasoning and exhaustive search: Quasigroup existence problems
- PSATO: A distributed propositional prover and its application to quasigroup problems
- Tools and algorithms for the construction and analysis of systems. 14th international conference, TACAS 2008, held as part of the joint European conferences on theory and practice of software, ETAPS 2008, Budapest, Hungary, March 29--April 6, 2008. Proceedings
- An interpolating theorem prover
- Solvable cases of the decision problem
- Compression of Propositional Resolution Proofs by Lowering Subproofs
- Generating Minimum Transitivity Constraints in P-time for Deciding Equality Logic
- Ground interpolation for the theory of equality
- Efficient generation of craig interpolants in satisfiability modulo theories
- Linear reasoning. A new form of the Herbrand-Gentzen theorem
- Counterexample-guided abstraction refinement for symbolic model checking
- Fast Decision Procedures Based on Congruence Closure
- Logic in Computer Science
- Two Techniques for Minimizing Resolution Proofs
- Lazy abstraction
- Interpolation and Symbol Elimination
- Exploiting Symmetry in SMT Problems
- Computer Aided Verification
- Computer Aided Verification
- Theory and Applications of Satisfiability Testing
- The MathSAT5 SMT Solver
- Rewriting-based Quantifier-free Interpolation for a Theory of Arrays.
- Automated Deduction – CADE-20
- Quantifier-free interpolation in combinations of equality interpolating theories
- A Decision Procedure for Bit-Vectors and Arrays
- Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic
- Lazy Abstraction with Interpolants
- Computer Aided Verification
This page was built for publication: Parallelizing SMT solving: lazy decomposition and conciliation
