Deciding Bit-Vector Formulas with mcSAT

DOI10.1007/978-3-319-40970-2_16zbMath1475.68226OpenAlexW2468832334MaRDI QIDQ2818018

Christoph M. Wintersteiger, Aleksandar Zeljić, Philipp Rümmer

Publication date: 5 September 2016

Published in: Theory and Applications of Satisfiability Testing – SAT 2016 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-40970-2_16

Mathematics Subject Classification ID

Logic in computer science (03B70) Computational aspects of satisfiability (68R07)

Related Items (5)

Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs ⋮ Propagation based local search for bit-precise reasoning ⋮ Conflict-driven satisfiability for theory combination: transition system and completeness ⋮ Wombit: a portfolio bit-vector solver using word-level propagation ⋮ Solving bitvectors with MCSAT: explanations from bits and pieces

Uses Software

• Boolector
• NuSMV
• Yices
• z3
• bv2epr
• CVC4
• MathSAT5
• SLAyer
• STP

Cites Work

• Unnamed Item
• Unnamed Item
• Cutting to the chase.
• On the Complexity of Symbolic Verification and Decision Problems in Bit-Vector Logic
• A Model-Constructing Satisfiability Calculus
• SAT-Based Model Checking without Unrolling
• Reconstruction of Z3’s Bit-Vector Proofs in HOL4 and Isabelle/HOL
• Solving SAT and SAT Modulo Theories
• An Alternative to SAT-Based Approaches for Bit-Vectors
• More on the Complexity of Quantifier-Free Fixed-Size Bit-Vector Logics with Binary Encoding
• Tools and Algorithms for the Construction and Analysis of Systems
• The MathSAT5 SMT Solver
• A Decision Procedure for Bit-Vectors and Arrays
• Computer Aided Verification

This page was built for publication: Deciding Bit-Vector Formulas with mcSAT