[Back]

L. Kovacs:
"Symbol Elimination in Program Analysis";
Keynote Lecture: 13th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC), Timisoara, Romania; 2011-09-26 - 2011-09-29; in: "Proc. of 13th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC)", D. Wang, V. Negru, T. Ida, T. Jebelean, D. Petcu, S. Watt, D. Zaharie (ed.); IEEE Computer Society, IEEE Computer Society Order Number P4630, BMS Part Number: CFP11387-PRT (2012), ISBN: 978-0-7695-4630-8; 12 - 13.

Automatic understanding of the intended meaning of computer programs is a very hard problem, requiring intelligence and reasoning. In this talk we present a new method for program analysis, called symbol elimination, that uses first-order theorem proving techniques to automatically discover non-trivial program properties, such as loop invariants and loop bounds. Moreover, symbol elimination can be used as an alternative to interpolation in software verification.

Automatic understanding of the intended meaning of computer programs is a very hard problem, requiring intelligence and reasoning. In this talk we present a new method for program analysis, called symbol elimination, that uses first-order theorem proving techniques to automatically discover non-trivial program properties, such as loop invariants and loop bounds. Moreover, symbol elimination can be used as an alternative to interpolation in software verification.

program verification, loop invariants, loop bounds, interpolants, theorem proving, symbolic computation

http://publik.tuwien.ac.at/files/PubDat_205748.pdf