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. © 2011 Springer-Verlag.
|Title of host publication||Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.|
|Number of pages||14|
|Publication status||Published - 2011|
|Event||10th Mexican International Conference on Artificial Intelligence, MICAI 2011 - Puebla|
Duration: 1 Jul 2011 → …
|Conference||10th Mexican International Conference on Artificial Intelligence, MICAI 2011|
|Period||1/07/11 → …|