A layered algorithm for quantifier elimination from linear modular constraints

DOI10.1007/s10703-016-0260-9zbMath1368.68332OpenAlexW2560512579MaRDI QIDQ2363817

Ajith K. John, Supratik Chakraborty

Publication date: 26 July 2017

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-016-0260-9

zbMATH Keywords

quantifier eliminationdecision diagramsbit-precise verificationlayered algorithmlinear modular arithmetic

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Numerical linear algebra (65F99)

Related Items (3)

Counterexample-Guided Model Synthesis ⋮ On solving quantified bit-vector constraints using invertibility conditions ⋮ Solving bitvectors with MCSAT: explanations from bits and pieces

Uses Software

• PVS
• CUDD
• z3
• LinAIG
• Spacer
• STP
• Mjollnir

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces
• SMT-based model checking for recursive programs
• A quantifier-elimination based heuristic for automatically generating inductive assertions for programs
• Efficiently solving quantified bit-vector formulas
• Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
• Fourier-Motzkin elimination and its dual
• Applying Linear Quantifier Elimination
• Linear reasoning. A new form of the Herbrand-Gentzen theorem
• Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations
• Linear Quantifier Elimination
• Graph-Based Algorithms for Boolean Function Manipulation
• A Decision Procedure for the First Order Theory of Real Addition with Order
• Monadic Decomposition
• Solving Difference Constraints over Modular Arithmetic
• Programming Languages and Systems
• Extending Quantifier Elimination to Linear Inequalities on Bit-Vectors
• A Decision Procedure for Bit-Vectors and Arrays
• A Quantifier Elimination Algorithm for Linear Real Arithmetic
• Diophantine Problems Over Local Fields I
• An algorithm for solving linear algebraic equations using residue arithmetic I
• Linear Quantifier Elimination as an Abstract Decision Procedure

This page was built for publication: A layered algorithm for quantifier elimination from linear modular constraints