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.