Deciding Bit-Vector Arithmetic with Abstraction

DOI10.1007/978-3-540-71209-1_28MaRDI QIDQ5758122zbMATH OpenOpenAlexFDO

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

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)

Recommendations

• A Decision Procedure for Bit-Vectors and Arrays
• Abstraction of bit-vector operations for BDD-based SMT solvers
• Deciding Bit-Vector Formulas with mcSAT
• Fast three-valued abstract bit-vector arithmetic
• Solving quantified bit-vector formulas using binary decision diagrams

Cited in

(27)

• Mind the gap: bit-vector interpolation recast over linear integer arithmetic
• URBiVA: uniform reduction to bit-vector arithmetic
• An alternative to SAT-based approaches for bit-vectors
• Computer Aided Verification
• Abstraction of bit-vector operations for BDD-based SMT solvers
• LCF-style bit-blasting in HOL4
• Matching multiplications in bit-vector formulas
• Deciding floating-point logic with abstract conflict driven clause learning
• Synthesis for Unbounded Bit-Vector Arithmetic
• SMT sampling via model-guided approximation
• Efficient combination of decision procedures for MUS computation
• Range and set abstraction using SAT
• Fast three-valued abstract bit-vector arithmetic
• Automatic verification of reduction techniques in higher order logic
• Automatic abstraction for bit-vectors using decision procedures
• Solving quantified bit-vector formulas using binary decision diagrams
• SAT-Based Model Checking
• Satisfiability modulo theories
• A Decision Procedure for Bit-Vectors and Arrays
• Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic
• Incremental bounded model checking for embedded software
• Proof-Guided Underapproximation Widening for Bounded Model Checking
• Proving LTL Properties of Bitvector Programs and Decompiled Binaries
• An approximation framework for solvers and decision procedures
• Complexity of fixed-size bit-vector logics
• Sharpening constraint programming approaches for bit-vector theory
• MedleySolver: online SMT algorithm selection

Describes a project that uses

Uses Software

• zChaff
• UCLID
• Yices
• Cogent
• MiniSat

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5758122)