Solving bitvectors with MCSAT: explanations from bits and pieces
From MaRDI portal
Publication:2096440
DOI10.1007/978-3-030-51074-9_7OpenAlexW3038318403MaRDI QIDQ2096440
Dejan Jovanović, Bruno Dutertre, Stéphane Graham-Lengrand
Publication date: 9 November 2022
Full work available at URL: https://arxiv.org/abs/2004.07940
Related Items (2)
Interpolation and model checking for nonlinear arithmetic ⋮ Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Decision procedures. An algorithmic point of view
- Sharpening constraint programming approaches for bit-vector theory
- 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
- A layered algorithm for quantifier elimination from linear modular constraints
- Computer aided verification. 19th international conference, CAV 2007, Berlin, Germany, July 3--7, 2007. Proceedings.
- Satisfiability modulo theories and assignments
- Deciding Bit-Vector Formulas with mcSAT
- A Model-Constructing Satisfiability Calculus
- Solving Nonlinear Integer Arithmetic with MCSAT
- Solving SAT and SAT Modulo Theories
- Simplify: a theorem prover for program checking
- Graph-Based Algorithms for Boolean Function Manipulation
- Solving quantified bit-vectors using invertibility conditions
This page was built for publication: Solving bitvectors with MCSAT: explanations from bits and pieces
