Sharpening constraint programming approaches for bit-vector theory
From MaRDI portal
Publication:2011567
DOI10.1007/978-3-319-59776-8_1zbMath1489.68249OpenAlexW2619890504MaRDI QIDQ2011567
François Bobot, Bruno Marre, Zakaria Chihani, Sébastien Bardin
Publication date: 4 August 2017
Full work available at URL: https://hal-cea.archives-ouvertes.fr/cea-01795779/file/bv-cpaior.pdf
Specification and verification (program logics, model checking, etc.) (68Q60) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items
Wombit: a portfolio bit-vector solver using word-level propagation, Solving bitvectors with MCSAT: explanations from bits and pieces, On the usefulness of linear modular arithmetic in constraint programming
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Solving quantified verification conditions using satisfiability modulo theories
- Social processes and proofs of theorems and programs
- Boosting search with variable elimination in constraint optimization and constraint satisfaction problems
- Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
- A Bit-Vector Solver with Word-Level Propagation
- Taking Satisfiability to the Next Level with Z3
- A Constraint Solver Based on Abstract Domains
- An Alternative to SAT-Based Approaches for Bit-Vectors
- Simplification by Cooperating Decision Procedures
- Explaining Time-Table-Edge-Finding Propagation for the Cumulative Resource Constraint
- Lazy abstraction
- Tools and Algorithms for the Construction and Analysis of Systems
- Theory and Applications of Satisfiability Testing
- The MathSAT5 SMT Solver
- A Decision Procedure for Bit-Vectors and Arrays
- Lazy Abstraction with Interpolants
- Deciding Bit-Vector Arithmetic with Abstraction
