Name
Abstract | ||
|---|---|---|
Automatic derivation of invariants is one of the critical conundrums in the framework of the inductive program verification methodologies. This paper presents a novel and simple approach to generating polynomial equations as loop invariants. Finite difference of expressions and linear equation solving are harnessed. Unlike related work, the generated constraints are linear equalities, which can be solved efficiently. Furthermore, invariants of higher degree can be constructed in terms of those of lower degree. The case studies demonstrate the effectiveness of the approach. |
Year | DOI | Venue |
|---|---|---|
2011 | 10.1007/978-3-642-21204-8_29 | FAW-AAIM |
Keywords | Field | DocType |
critical conundrum,linear equation,linear equality,simple approach,loop invariants,lower degree,finite difference,higher degree,case study,automatic derivation,iterative method,loop invariant | Linear equation,Expression (mathematics),Algebra,Polynomial,Mathematical analysis,Iterative method,Finite difference,Loop invariant,Invariant (mathematics),Mathematics | Conference |
Volume | ISSN | Citations |
6681 | 0302-9743 | 0 |
PageRank | References | Authors |
0.34 | 9 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Shikun Chen | 1 | 0 | 1.01 |
| Zhoujun Li | 2 | 964 | 115.99 |
| Xiaoyu Song | 3 | 318 | 46.99 |
| Mengjun Li | 4 | 57 | 7.72 |