An Iterative Method for Generating Loop Invariants
From MaRDI portal
Publication:3004678
DOI10.1007/978-3-642-21204-8_29zbMath1329.68074MaRDI 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
68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
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