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

fYear

2005

fDate

25-29 Sept. 2005

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Symbolic and Numeric Algorithms for Scientific Computing, 2005. SYNASC 2005. Seventh International Symposium on

Print_ISBN

0-7695-2453-2

Type

conf

DOI

10.1109/SYNASC.2005.19

Filename

1595857