Loading...
Please wait, while we are loading the content...
Automatic Generation of Polynomial Loop Invariants for Imperative Programs ?
| Content Provider | Semantic Scholar |
|---|---|
| Author | Carbonell, Enric Kapur, Deepak |
| Abstract | A general framework is presented for automating the discovery of loop invariants for imperative programs. Theoretical results about the correctness and completeness of the proposed method are given. More importantly, it is shown how this abstract approach can be used to automatically infer polynomial invariants. The method has been implemented in Maple. Evidence of its practical interest is shown by means of several non-trivial examples, for which the polynomial loop invariants generated are directly applicable for proving correctness by means of a simple verifier. |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | http://www.cs.unm.edu/~moore/tr/03-10/invpaper3.pdf |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
