Name
Abstract | ||
|---|---|---|
We present a generic symbolic analysis framework for imperative programming languages. Our framework is capable of computing all valid variable bindings of a program at given program points. This information is invaluable for domain-specific static program analyses such as memory leak detection, program parallelisation, and the detection of superfluous bound checks, variable aliases and task deadlocks. We employ path expression algebra to model the control flow information of programs. A homomorphism maps path expressions into the symbolic domain. At the center of the symbolic domain is a compact algebraic structure called supercontext. A supercontext contains the complete control and data flow analysis information valid at a given program point. Our approach to compute supercontexts is based purely on algebra and is fully automated. This novel representation of program semantics closes the gap between program analysis and computer algebra systems, which makes supercontexts an ideal intermediate representation for all domain-specific static program analyses. Our approach is more general than existing methods because it can derive solutions for arbitrary (even intra-loop) nodes of reducible and irreducible control flow graphs. We prove the correctness of our symbolic analysis method. Our experimental results show that the problem sizes arising from real-world applications such as the SPEC95 benchmark suite are tractable for our symbolic analysis framework. |
Year | DOI | Venue |
|---|---|---|
2006 | 10.1007/11860990_12 | JMLC |
Keywords | Field | DocType |
symbolic analysis framework,domain-specific static program,imperative programming language,program analysis,program parallelisation,data flow analysis information,program semantics,program point,symbolic domain,generic symbolic analysis framework,domain-specific static program analysis,symbolic analysis,memory leaks,path expressions,intermediate representation,programming language | Computer science,Symbolic computation,Data-flow analysis,Theoretical computer science,Symbolic programming,Control flow analysis,Symbolic data analysis,Symbolic execution,Program analysis,Symbolic trajectory evaluation | Conference |
Volume | ISSN | ISBN |
4228 | 0302-9743 | 3-540-40927-0 |
Citations | PageRank | References |
5 | 0.44 | 24 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Bernd Burgstaller | 1 | 133 | 17.54 |
| Bernhard Scholz | 2 | 104 | 10.59 |
| Johann Blieberger | 3 | 158 | 19.01 |