Extending Quantifier Elimination to Linear Inequalities on Bit-Vectors

DOI10.1007/978-3-642-36742-7_6zbMATH Open1381.68055OpenAlexW1769016125MaRDI QIDQ5326316FDOQ5326316

Authors: Ajith K. John, Supratik Chakraborty 

Publication date: 5 August 2013

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-642-36742-7_6

Recommendations

• Weak Integer Quantifier Elimination Beyond the Linear Case
• Efficiently solving quantified bit-vector formulas
• On solving quantified bit-vector constraints using invertibility conditions
• A Quantifier Elimination Algorithm for Linear Real Arithmetic
• Solving quantified bit-vectors using invertibility conditions
• Quantifier elimination for linear modular constraints
• Linear quantifier elimination
• Linear Quantifier Elimination
• More on the complexity of quantifier-free fixed-size bit-vector logics with binary encoding

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70)

Cited In (4)

• A layered algorithm for quantifier elimination from linear modular constraints
• Quantifier elimination for linear modular constraints
• Efficient handling of universally quantified inequalities
• Sharpening constraint programming approaches for bit-vector theory

This page was built for publication: Extending Quantifier Elimination to Linear Inequalities on Bit-Vectors

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