Truncating abstraction of bit-vector operations for BDD-based SMT solvers

DOI10.1016/J.TCS.2024.114664MaRDI QIDQ6589830zbMATH OpenFDO

Authors Martin Jonáš, Jan Strejček

Publication date 20 August 2024

Published in Theoretical Computer Science (Search for Journal in Brave)

zbMATH Keywords

SMT solvingbit-vector theoryoperation abstractionQ3B

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Cites work

• Abstraction of bit-vector operations for BDD-based SMT solvers
• Complexity of fixed-size bit-vector logics
• Constraint-Based Invariant Inference over Predicate Abstraction
• Counterexample-Guided Model Synthesis
• Deciding Bit-Vector Formulas with mcSAT
• Efficiently solving quantified bit-vector formulas
• From program verification to program synthesis
• Graph-Based Algorithms for Boolean Function Manipulation
• On simplification of formulas with unconstrained variables and quantifiers
• On the complexity of VLSI implementations and graph representations of Boolean functions with application to integer multiplication
• Ranking function synthesis for bit-vector relations
• Satisfiability modulo theories
• Solving quantified bit-vector formulas using binary decision diagrams
• Solving quantified bit-vectors using invertibility conditions
• Tools and algorithms for the construction and analysis of systems. 14th international conference, TACAS 2008, held as part of the joint European conferences on theory and practice of software, ETAPS 2008, Budapest, Hungary, March 29--April 6, 2008. Procee

This page was built for publication: Truncating abstraction of bit-vector operations for BDD-based SMT solvers

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