Name
Abstract | ||
|---|---|---|
Automatic understanding of the intended meaning of computer programs is a very hard problem, requiring intelligence and reasoning. In this abstract we discuss a new method for program analysis, called symbol elimination. Symbol elimination 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 for software verification. |
Year | DOI | Venue |
|---|---|---|
2011 | 10.1109/SYNASC.2011.60 | SYNASC |
Keywords | Field | DocType |
intended meaning,symbol elimination,first-order theorem,program analysis,hard problem,computer program,automatic understanding,loop bound,loop invariants,non-trivial program property,theorem proving,computational modeling,cognition,interpolation,computability,formal verification,software verification,symbolic computation,first order,color,computer model | Discrete mathematics,Computer science,Symbol,Interpolation,Automated theorem proving,Theoretical computer science,Computability,Loop invariant,Program analysis,Software verification,Formal verification | Conference |
ISSN | ISBN | Citations |
2470-8801 | 978-1-4673-0207-4 | 0 |
PageRank | References | Authors |
0.34 | 3 | 1 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Laura Kovács | 1 | 494 | 36.97 |