[Back]


Talks and Poster Presentations (with Proceedings-Entry):

K. Hoder, L. Kovacs, A. Voronkov:
"Case Studies on Invariant Generation Using a Saturation Theorem Prover";
Talk: 10th Mexican International Conference on Artificial Intelligence (MICAI), Puebla, Mexico; 11-26-2011 - 12-04-2011; in: "Advances in Artificial Intelligence - 10th Mexican International Conference on Artificial Intelligence (MICAI)", I. Batyrshin, G. Sidorov (ed.); Springer, LNAI 7094 (2011), ISBN: 978-3-642-25323-2; 1 - 15.



English abstract:
Automatic understanding of the intended meaning of computer programs is a very hard problem, requiring intelligence and reasoning.
In this paper we evaluate a program analysis method, called symbol elimination, that uses first-order theorem proving techniques to automatically discover non-trivial program properties. We discuss implementation details of the method, present experimental results, and discuss the relation of the program properties obtained by our implementation and the intended meaning of the programs used in the experiments.

German abstract:
Automatic understanding of the intended meaning of computer programs is a very hard problem, requiring intelligence and reasoning.
In this paper we evaluate a program analysis method, called symbol elimination, that uses first-order theorem proving techniques to automatically discover non-trivial program properties. We discuss implementation details of the method, present experimental results, and discuss the relation of the program properties obtained by our implementation and the intended meaning of the programs used in the experiments.

Keywords:
program verification, loop invariants, theorem proving


Electronic version of the publication:
http://publik.tuwien.ac.at/files/PubDat_205742.pdf


Created from the Publication Database of the Vienna University of Technology.