The Community for Technology Leaders
2011 13th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (2005)
Timisoara, Romania
Sept. 25, 2005 to Sept. 29, 2005
ISBN: 0-7695-2453-2
pp: 245-249
Laura Ildikó Kovács , Johannes Kepler University and Institute e-Austria
Tudor Jebelean , Johannes Kepler University and Institute e-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.
INDEX TERMS
null
CITATION
Laura Ildikó Kovács, Tudor Jebelean, "An Algorithm for Automated Generation of Invariants for Loops with Conditionals", 2011 13th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, vol. 00, no. , pp. 245-249, 2005, doi:10.1109/SYNASC.2005.19
80 ms
(Ver 3.3 (11022016))