Name
Abstract | ||
|---|---|---|
In an earlier paper, an algorithm based on algebraic geometry was developed for discovering polynomial invariants in loops without nesting, not requiring any a priori bound on the degree of the invariants. Polynomial invariants were shown to form an ideal, a basis of which could be computed using Gröbner bases methods. In this paper, an abstract logical framework is presented for automating the discovery of invariants for loops without nesting, of which the algorithm based on algebraic geometry and Gröbner bases is one particular instance. The approach based on this logical abstract framework is proved to be correct and complete. The techniques have been used with a verifier to automatically check properties of many non-trivial programs with considerable success. Some of these programs are discussed in the paper to illustrate the effectiveness of the method. |
Year | DOI | Venue |
|---|---|---|
2004 | 10.1007/978-3-540-31862-0_24 | ICTAC |
Keywords | Field | DocType |
bner bases method,non-trivial program,considerable success,abstract logical framework,program verification,particular instance,polynomial invariants,bner base,earlier paper,automatic generation,logical abstract framework,algebraic geometry,logical framework | Discrete mathematics,Algebraic geometry,Polynomial,Computer science,A priori and a posteriori,Automated theorem proving,Invariant (mathematics),Linear inequality,Logical framework | Conference |
Volume | ISSN | ISBN |
3407 | 0302-9743 | 3-540-25304-1 |
Citations | PageRank | References |
20 | 0.82 | 10 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Enric Rodríguez-Carbonell | 1 | 446 | 26.13 |
| Deepak Kapur | 2 | 2282 | 235.00 |