A quantifier-elimination based heuristic for automatically generating inductive assertions for programs

DOI10.1007/S11424-006-0307-XzbMath1115.68051OpenAlexW2159289729MaRDI QIDQ882517

Deepak Kapur

Publication date: 24 May 2007

Published in: Journal of Systems Science and Complexity (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s11424-006-0307-x

zbMATH Keywords

quantifier eliminationloop invariantautomated software analysis and verificationinductive assertion

Mathematics Subject Classification ID

General topics in the theory of software (68N01) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (12)

A layered algorithm for quantifier elimination from linear modular constraints ⋮ When Is a Formula a Loop Invariant? ⋮ On invariant checking ⋮ A survey on algorithms for computing comprehensive Gröbner systems and comprehensive Gröbner bases ⋮ Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants ⋮ Elimination Techniques for Program Analysis ⋮ TERMINATION ANALYSIS OF LINEAR LOOPS ⋮ Reasoning Algebraically About P-Solvable Loops ⋮ On invariant synthesis for parametric systems ⋮ Synthesizing Switching Controllers for Hybrid Systems by Generating Invariants ⋮ Discovering non-terminating inputs for multi-path polynomial programs ⋮ On interpolation in automated theorem proving

Uses Software

• Unnamed Item
• REDLOG
• RRL

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The complexity of almost linear diophantine problems
• Weak quantifier elimination for the full linear theory of the integers
• Basic principles of mechanical theorem proving in elementary geometries
• A refutational approach to geometry theorem proving
• Partial cylindrical algebraic decomposition for quantifier elimination
• Comprehensive Gröbner bases
• Affine relationships among variables of a program
• Applying Linear Quantifier Elimination
• Non-linear loop invariant generation using Gröbner bases
• Precise interprocedural analysis through linear algebra
• Logical analysis of programs
• Automatic Generation of Polynomial Loop Invariants
• The synthesis of loop predicates
• Static Analysis
• Theoretical Aspects of Computing - ICTAC 2004
• Computer Aided Verification

This page was built for publication: A quantifier-elimination based heuristic for automatically generating inductive assertions for programs