Sharpening constraint programming approaches for bit-vector theory
type: Item
instance of: scholarly article
title: Sharpening constraint programming approaches for bit-vector theory
zbMATH Open document ID: 1489.68249
DOI: 10.1007/978-3-319-59776-8_1
author: Zakaria Chihani
author: Bruno Marre
author: François Bobot
author: Sébastien Bardin
publication date: 2017-08-04T00:00:00Z
full work available at URL: bv-cpaior.pdf
Mathematics Subject Classification ID: 68T20
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 68V15
zbMATH DE Number: 6756571
describes a project that uses: Boolector
describes a project that uses: GATeL
describes a project that uses: CBMC
describes a project that uses: BINSEC/SE
describes a project that uses: STP
describes a project that uses: MiniSat
describes a project that uses: Yices
describes a project that uses: z3
describes a project that uses: CPBPV
describes a project that uses: SMT-LIB
describes a project that uses: Chaff
describes a project that uses: CVC4
describes a project that uses: MathSAT5
describes a project that uses: OSMOSE
describes a project that uses: TCAS
MaRDI profile type: Publication
OpenAlex ID: W2619890504
cites work: An Alternative to SAT-Based Approaches for Bit-Vectors
cites work: Solving quantified verification conditions using satisfiability modulo theories
cites work: Taking Satisfiability to the Next Level with Z3
cites work: Deciding Bit-Vector Arithmetic with Abstraction
cites work: The MathSAT5 SMT Solver
cites work: Tools and Algorithms for the Construction and Analysis of Systems
cites work: Boosting search with variable elimination in constraint optimization and constraint satisfaction problems
cites work: Q4144755
cites work: Theory and Applications of Satisfiability Testing
cites work: Explaining Time-Table-Edge-Finding Propagation for the Cumulative Resource Constraint
cites work: A Decision Procedure for Bit-Vectors and Arrays
cites work: Q2767075
cites work: Lazy abstraction
cites work: Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
cites work: Lazy Abstraction with Interpolants
cites work: Social processes and proofs of theorems and programs
cites work: Simplification by Cooperating Decision Procedures
cites work: A Constraint Solver Based on Abstract Domains
cites work: A Bit-Vector Solver with Word-Level Propagation
Recommended article: Towards satisfiability modulo parametric bit-vectors
Recommended article: On solving quantified bit-vector constraints using invertibility conditions
Recommended article: An Alternative to SAT-Based Approaches for Bit-Vectors
Recommended article: Bit-vector algorithms for binary constraint satisfaction and subgraph isomorphism
Recommended article: Q3455636
Recommended article: Synthesis of Domain Specific CNF Encoders for Bit-Vector Solvers
Recommended article: Efficiently solving quantified bit-vector formulas
Recommended article: Extending Quantifier Elimination to Linear Inequalities on Bit-Vectors
Recommended article: Abstraction of bit-vector operations for BDD-based SMT solvers
description: scientific article; zbMATH DE number 6756571