An iterative method for generating loop invariants

DOI10.1007/978-3-642-21204-8_29MaRDI QIDQ3004678zbMATH OpenOpenAlexFDO

Authors Shikun Chen, Zhoujun Li, Xiaoyu Song, Mengjun Li

Publication date 3 June 2011

Published in Frontiers in Algorithmics and Algorithmic Aspects in Information and Management (Search for Journal in Brave)

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

zbMATH Keywords

finite differenceloop invariantprogram correctness

Mathematics Subject Classification ID

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

Recommendations

• Automatic generation of polynomial invariants of bounded degree using abstract interpretation
• Automatic generation of non-linear loop invariants
• Generating all polynomial invariants in simple loops
• Static Analysis
• Theoretical Aspects of Computing - ICTAC 2004

Cites work

• Automatic generation of polynomial invariants of bounded degree using abstract interpretation
• Computing polynomial program invariants
• Generating Polynomial Invariants with DISCOVERER and QEPCAD
• Generating all polynomial invariants in simple loops
• Non-linear loop invariant generation using Gröbner bases
• Precise interprocedural analysis through linear algebra
• Reasoning Algebraically About P-Solvable Loops
• Static analysis. 11th international symposium, SAS 2004, Verona, Italy, August 26--28, 2004. Proceedings.
• The octagon abstract domain
• Verification, Model Checking, and Abstract Interpretation

Cited in

(17)

• Loop Invariants from Counterexamples
• scientific article; zbMATH DE number 1098500 (Why is no real title available?)
• Loop invariants in floating point algorithms
• Inferring Loop Invariants Using Postconditions
• Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops
• Automatic generation of polynomial invariants of bounded degree using abstract interpretation
• A method for computing the number of iterations in data dependent loops
• Automatically inferring loop invariants via algorithmic learning
• Automatic generation of non-linear loop invariants
• Loop Analysis by Quantification over Iterations
• Automatic proving or disproving equality loop invariants based on finite difference techniques
• When is a formula a loop invariant?
• Programming Languages and Systems
• Automated generation of loop invariants by recurrence solving in \texttt{Theorema}
• Elimination of loop invariants in program verification
• SMT-based array invariant generation
• Non-linear loop invariant generation using Gröbner bases

This page was built for publication: An iterative method for generating loop invariants

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