Name
Abstract | ||
|---|---|---|
Path explosion is a major issue in applying path-sensitive symbolic analysis to large programs. We observe that many symbolic states generated by the symbolic analysis of a procedure are indistinguishable to its callers. It is, therefore, possible to keep only one state from each set of equivalent symbolic states without affecting the analysis result. Based on this observation, we propose an equivalence relation called z-equivalence, which is weaker than logical equivalence, to relate a large number of z-equivalent states. We prove that z-equivalence is strong enough to guarantee that paths to be traversed by the symbolic analysis of two z-equivalent states are identical, giving the same solutions to satisfiability and validity queries. We propose a sound linear algorithm to detect z-equivalence. Our experiments show that the symbolic analysis that leverages z-equivalence is able to achieve more than ten orders of magnitude reduction in terms of search space. The reduction significantly alleviates the path explosion problem, enabling us to apply symbolic analysis in large programs such as Hadoop and Linux Kernel. |
Year | DOI | Venue |
|---|---|---|
2014 | 10.1145/2652484 | ACM Trans. Softw. Eng. Methodol. |
Keywords | Field | DocType |
algorithms,experimentation,state equivalence detection,symbolic analysis,path explosion,verification,software/program verification,performance | The Symbolic,Logical equivalence,Equivalence relation,Computer science,Satisfiability,Algorithm,Theoretical computer science,Symbolic data analysis,Scaling,Linux kernel,Symbolic trajectory evaluation | Journal |
Volume | Issue | ISSN |
23 | 4 | 1049-331X |
Citations | PageRank | References |
3 | 0.37 | 26 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Yueqi Li | 1 | 3 | 0.37 |
| S. C. Cheung | 2 | 2657 | 162.89 |
| Xiangyu Zhang | 3 | 2857 | 151.00 |
| Yepang Liu | 4 | 415 | 24.58 |