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

DOI10.1007/S11424-006-0307-XMaRDI QIDQ882517zbMATH OpenOpenAlexFDO

Authors 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

loop invariantquantifier eliminationautomated 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)

Recommendations

• Elimination Techniques for Program Analysis
• Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants
• Theoretical Aspects of Computing - ICTAC 2004
• Synthesizing invariants by solving solvable loops
• Ilinva: using abduction to generate loop invariants

Cites work

• scientific article; zbMATH DE number 3586510 (Why is no real title available?)
• scientific article; zbMATH DE number 1234104 (Why is no real title available?)
• scientific article; zbMATH DE number 1253963 (Why is no real title available?)
• scientific article; zbMATH DE number 1948385 (Why is no real title available?)
• A refutational approach to geometry theorem proving
• Affine relationships among variables of a program
• Applying Linear Quantifier Elimination
• Automatic Generation of Polynomial Loop Invariants
• Basic principles of mechanical theorem proving in elementary geometries
• Comprehensive Gröbner bases
• Computer Aided Verification
• Logical analysis of programs
• Non-linear loop invariant generation using Gröbner bases
• Partial cylindrical algebraic decomposition for quantifier elimination
• Precise interprocedural analysis through linear algebra
• Static Analysis
• The complexity of almost linear diophantine problems
• The synthesis of loop predicates
• Theoretical Aspects of Computing - ICTAC 2004
• Weak quantifier elimination for the full linear theory of the integers

Cited in

(15)

• Synthesizing switching controllers for hybrid systems by generating invariants
• Ilinva: using abduction to generate loop invariants
• On invariant checking
• Reasoning Algebraically About P-Solvable Loops
• A survey on algorithms for computing comprehensive Gröbner systems and comprehensive Gröbner bases
• TERMINATION ANALYSIS OF LINEAR LOOPS
• Discovering non-terminating inputs for multi-path polynomial programs
• On invariant synthesis for parametric systems
• A layered algorithm for quantifier elimination from linear modular constraints
• When is a formula a loop invariant?
• On interpolation in automated theorem proving
• Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants
• Reasoning about loops using Vampire in KeY
• Elimination Techniques for Program Analysis
• Lingva: generating and proving program properties using symbol elimination

Describes a project that uses

Uses Software

• RRL
• REDLOG
• QEPCAD

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

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