Solving quantified bit-vectors using invertibility conditions

DOI10.1007/978-3-319-96142-2_16MaRDI QIDQ6039405zbMATH OpenOpenAlexFDO

Authors Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett, Cesare Tinelli

Publication date 5 May 2023

Published in Computer Aided Verification (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-319-96142-2_16

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Recommendations

• On solving quantified bit-vector constraints using invertibility conditions
• Solving quantified bit-vector formulas using binary decision diagrams
• Counterexample-Guided Model Synthesis
• Efficiently solving quantified bit-vector formulas
• Abstraction of bit-vector operations for BDD-based SMT solvers

Cited in

(16)

• Abstraction of bit-vector operations for BDD-based SMT solvers
• Preface of the special issue on the conference on computer-aided verification 2018
• On solving quantified bit-vector constraints using invertibility conditions
• Towards satisfiability modulo parametric bit-vectors
• Solving bitvectors with MCSAT: explanations from bits and pieces
• Towards bit-width-independent proofs in SMT solvers
• Efficiently solving quantified bit-vector formulas
• Solving quantified bit-vector formulas using binary decision diagrams
• Synthesis of domain specific CNF encoders for bit-vector solvers
• Extending Quantifier Elimination to Linear Inequalities on Bit-Vectors
• Invertibility conditions for floating-point formulas
• QSMA: A New Algorithm for Quantified Satisfiability Modulo Theory and Assignment
• Formal Verification of Bit-Vector Invertibility Conditions in Coq
• Truncating abstraction of bit-vector operations for BDD-based SMT solvers
• Solving hard Mizar problems with instantiation and strategy invention
• The QSMA algorithm for quantifiers in SMT

This page was built for publication: Solving quantified bit-vectors using invertibility conditions

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