QSMA: A New Algorithm for Quantified Satisfiability Modulo Theory and Assignment
From MaRDI portal
Publication:6492731
DOI10.1007/978-3-031-38499-8_5MaRDI QIDQ6492731
Stéphane Graham-Lengrand, Unnamed Author, Maria Paola Bonacina
Publication date: 26 April 2024
Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Cites Work
- Unnamed Item
- On deciding satisfiability by theorem proving with speculative inferences
- SMT-based model checking for recursive programs
- Interpolation and model checking for nonlinear arithmetic
- Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs
- Solving bitvectors with MCSAT: explanations from bits and pieces
- Conflict-driven satisfiability for theory combination: transition system and completeness
- Solving Non-linear Arithmetic
- A Model-Constructing Satisfiability Calculus
- Simplify: a theorem prover for program checking
- Integrating Linear Arithmetic into Superposition Calculus
- Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
- Efficient E-Matching for SMT Solvers
- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
- Superposition Modulo Linear Arithmetic SUP(LA)
- Hierarchic Superposition with Weak Abstraction
- Solving quantified bit-vectors using invertibility conditions
This page was built for publication: QSMA: A New Algorithm for Quantified Satisfiability Modulo Theory and Assignment
