Solving bitvectors with MCSAT: explanations from bits and pieces
From MaRDI portal
Publication:2096440
Cites work
- A layered algorithm for quantifier elimination from linear modular constraints
- A model-constructing satisfiability calculus
- Computer aided verification. 19th international conference, CAV 2007, Berlin, Germany, July 3--7, 2007. Proceedings.
- Computer aided verification. 26th international conference, CAV 2014, held as part of the Vienna summer of logic, VSL 2014, Vienna, Austria, July 18--22, 2014. Proceedings
- Conflict-driven satisfiability for theory combination: transition system and completeness
- Deciding Bit-Vector Formulas with mcSAT
- Decision procedures. An algorithmic point of view
- Graph-Based Algorithms for Boolean Function Manipulation
- Handbook of automated reasoning. In 2 vols
- scientific article; zbMATH DE number 5493266 (Why is no real title available?)
- Satisfiability modulo theories and assignments
- Sharpening constraint programming approaches for bit-vector theory
- Simplify: a theorem prover for program checking
- Solving nonlinear integer arithmetic with MCSAT
- Solving quantified bit-vectors using invertibility conditions
- Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
Cited in
(7)- Deciding Bit-Vector Formulas with mcSAT
- QSMA: A New Algorithm for Quantified Satisfiability Modulo Theory and Assignment
- Boosting MCSat modulo nonlinear integer arithmetic via local search
- The QSMA algorithm for quantifiers in SMT
- MCSat-based finite field reasoning in the \textsc{Yices2} SMT solver (short paper)
- Interpolation and model checking for nonlinear arithmetic
- Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs
This page was built for publication: Solving bitvectors with MCSAT: explanations from bits and pieces
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2096440)
