[Zurück]


Vorträge und Posterpräsentationen (mit Tagungsband-Eintrag):

L. Kovacs:
"Symbol Elimination in Program Analysis";
Hauptvortrag: 13th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC), Timisoara, Romania; 26.09.2011 - 29.09.2011; 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 (Hrg.); IEEE Computer Society, IEEE Computer Society Order Number P4630, BMS Part Number: CFP11387-PRT (2012), ISBN: 978-0-7695-4630-8; S. 12 - 13.



Kurzfassung deutsch:
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.

Kurzfassung englisch:
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.

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


Elektronische Version der Publikation:
http://publik.tuwien.ac.at/files/PubDat_205748.pdf


Erstellt aus der Publikationsdatenbank der Technischen Universität Wien.