Seventh International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'05) (2005)
Sept. 25, 2005 to Sept. 29, 2005
Laura Ildikó Kovács , Johannes Kepler University and Institute e-Austria
Tudor Jebelean , Johannes Kepler University and Institute e-Austria
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.
L. I. Kovács and T. Jebelean, "An Algorithm for Automated Generation of Invariants for Loops with Conditionals," Seventh International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'05)(SYNASC), Timisoara, Romania, 2005, pp. 245-249.