Deciding Bit-Vector Arithmetic with Abstraction

DOI10.1007/978-3-540-71209-1_28zbMath1186.68281OpenAlexW1919297764MaRDI QIDQ5758122

Daniel Kroening, Bryan A. Brady, Sanjit A. Seshia, Joël Ouaknine, Randal E. Bryant, Ofer Strichman

Publication date: 3 September 2007

Published in: Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-71209-1_28

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (14)

An approximation framework for solvers and decision procedures ⋮ Mind the Gap: Bit-vector Interpolation recast over Linear Integer Arithmetic ⋮ SAT-Based Model Checking ⋮ Satisfiability Modulo Theories ⋮ Incremental bounded model checking for embedded software ⋮ SMT sampling via model-guided approximation ⋮ Automatic verification of reduction techniques in higher order logic ⋮ Complexity of fixed-size bit-vector logics ⋮ Sharpening constraint programming approaches for bit-vector theory ⋮ URBiVA: Uniform Reduction to Bit-Vector Arithmetic ⋮ Solving Quantified Bit-Vector Formulas Using Binary Decision Diagrams ⋮ LCF-Style Bit-Blasting in HOL4 ⋮ Efficient Combination of Decision Procedures for MUS Computation ⋮ MedleySolver: online SMT algorithm selection

Uses Software

• MiniSat
• Cogent
• Yices
• UCLID
• zChaff

This page was built for publication: Deciding Bit-Vector Arithmetic with Abstraction