Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants

DOI10.1007/978-3-642-36675-8_11zbMath1385.68013MaRDI QIDQ4913868

Zhi-Hai Zhang, Matthias Horbach, Deepak Kapur, Qi Lu, Thanhvu H. Nguyen, Heng-Jun Zhao

Publication date: 16 April 2013

Published in: Automated Reasoning and Mathematics (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-36675-8_11

Mathematics Subject Classification ID

68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)

03C10: Quantifier elimination, model completeness, and related topics

Related Items

Certified Reasoning with Infinity, On interpolation in automated theorem proving, Speeding up the Constraint-Based Method in Difference Logic

Uses Software

• ASTREE

Cites Work

• Unnamed Item
• Unnamed Item
• Recent advances in program verification through computer algebra
• Termination of linear programs with nonlinear constraints
• A quantifier-elimination based heuristic for automatically generating inductive assertions for programs
• Hard problems in max-algebra, control theory, hypergraphs and other areas
• Applying Linear Quantifier Elimination
• Abstractions from proofs
• Non-linear loop invariant generation using Gröbner bases
• Constraint-Based Approach for Analysis of Hybrid Systems
• Inferring Min and Max Invariants Using Max-Plus Polyhedra
• Max-linear Systems: Theory and Algorithms
• Synthesizing Switching Logic Using Constraint Solving
• Avoiding exponential explosion
• Verification and synthesis using real quantifier elimination
• From program verification to program synthesis
• Abstract Interpretation Frameworks
• Programming Languages and Systems
• An Improved Tight Closure Algorithm for Integer Octagonal Constraints
• Ranking Abstractions
• Max-Plus Convex Geometry
• An axiomatic basis for computer programming
• Theory and Applications of Satisfiability Testing