Title :
An algorithm for automated generation of invariants for loops with conditionals
Author :
Kovács, Laura Ildikó ; Jebelea, Tudor
Author_Institution :
Res. Inst. for Symbolic Comput., Johannes Kepler Univ., Linz, Austria
Abstract :
We present an algorithm that generates automatically (algebraic) invariant properties of a loop with conditionals. In the proposed algorithm program analysis is performed in order to transform the code into a form for which algebraic and combinatorial techniques can be applied to obtain invariant properties. These invariants are then used for verifying partial correctness of imperative programs in the Theorema system (www.theorema.org). The application of the method is demonstrated in few examples.
Keywords :
program compilers; program control structures; program diagnostics; program verification; Theorema system; algebraic invariant properties; algebraic techniques; algorithm program analysis; automated invariant generation; code transformation; combinatorial techniques; conditional loop; imperative programs; partial correctness verification; Algebra; Algorithm design and analysis; Computer languages; Difference equations; Inference algorithms; Logic design; Logic programming; Performance analysis; Polynomials; Power system modeling;
Conference_Titel :
Symbolic and Numeric Algorithms for Scientific Computing, 2005. SYNASC 2005. Seventh International Symposium on
Print_ISBN :
0-7695-2453-2
DOI :
10.1109/SYNASC.2005.19
