Truncating abstraction of bit-vector operations for BDD-based SMT solvers
From MaRDI portal
Publication:6589830
DOI10.1016/J.TCS.2024.114664MaRDI QIDQ6589830FDOQ6589830
Authors: Martin Jonáš, Jan Strejček 
Publication date: 20 August 2024
Published in: Theoretical Computer Science (Search for Journal in Brave)
Cites Work
- Graph-Based Algorithms for Boolean Function Manipulation
- Efficiently solving quantified bit-vector formulas
- Satisfiability modulo theories
- Complexity of fixed-size bit-vector logics
- 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. Proceedings
- Constraint-Based Invariant Inference over Predicate Abstraction
- Deciding Bit-Vector Formulas with mcSAT
- From program verification to program synthesis
- On simplification of formulas with unconstrained variables and quantifiers
- Abstraction of bit-vector operations for BDD-based SMT solvers
- Ranking function synthesis for bit-vector relations
- Solving quantified bit-vector formulas using binary decision diagrams
- Counterexample-Guided Model Synthesis
- Solving quantified bit-vectors using invertibility conditions
- On the complexity of VLSI implementations and graph representations of Boolean functions with application to integer multiplication
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)
