Name
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. |
Year | DOI | Venue |
|---|---|---|
2011 | 10.1007/978-3-642-25324-9_1 | MICAI |
Keywords | Field | DocType |
program analysis method,intended meaning,first-order theorem,program property,hard problem,computer program,automatic understanding,present experimental result,saturation theorem prover,invariant generation,implementation detail,case study,non-trivial program property | Symbol,Computer science,Automated theorem proving,Theoretical computer science,Invariant (mathematics),Program analysis | Conference |
Volume | ISSN | Citations |
7094 | 0302-9743 | 7 |
PageRank | References | Authors |
0.66 | 10 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Kryštof Hoder | 1 | 157 | 6.63 |
| Laura Kovács | 2 | 494 | 36.97 |
| Andrei Voronkov | 3 | 2670 | 225.46 |