Loading...
Please wait, while we are loading the content...
Similar Documents
Generation of Loop Invariants in Theorema by Combinatorial and Algebraic Methods
| Content Provider | Semantic Scholar |
|---|---|
| Author | Kovács, Laura Ildikó Jebelean, Tudor |
| Copyright Year | 2004 |
| Abstract | When generating verification conditions for a program, one is faced with one major task, namely with the situation when some additional assertions are needed (e.g. loop invariants). These assertions have the property that either they are invariant during execution of the program, or they depend on some other invariant properties. Therefore, automated formal verification is sensitive to the automated generation of invariants. In this paper, we present an alternative to expecting programmers to fully annotate code with invariants, namely a method for automatic generation of invariants from the program itself, using combinatorial algorithms and equational elimination, as well as an ongoing research work with some results based on applications of polynomial ideal theory. The implementation and the verification process is done in a prototype verification condition generator for imperative programs, which is part of the T oremasystem, a computer aided mathematical assistant that offers automated reasoning and computer algebra facilities for the working mathematician. The verification conditions for programs containing loops are generated fully automatically, in a form which can be immediately used by the automatic provers of Theoremain order to check whether they hold. We illustrate the effectiveness of our method by few examples. |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | http://www.risc.jku.at/publications/download/risc_461/2004-05-23-A.pdf |
| Alternate Webpage(s) | http://www.risc.uni-linz.ac.at/publications/download/risc_461/2004-05-23-A.pdf |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
