An Iterative Method for Generating Loop Invariants

DOI10.1007/978-3-642-21204-8_29zbMath1329.68074OpenAlexW115316089MaRDI QIDQ3004678

Shikun Chen, Xiaoyu Song, Zhou-Jun Li, 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)

Cites Work

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

This page was built for publication: An Iterative Method for Generating Loop Invariants