A Scalable Inclusion Constraint Solver Using Unification |
Ye Zhang, Flemming Nielsen
|
| Abstract | We describe a parameterized framework with which users can take advantage of unification over analysis variables to implement efficient or precise analyses, or even both. To be illustrative we instantiate the framework with reaching definition analysis and conduct a systematic evaluation of performance and precision of the analysis. We compare our result with that of a state-of-the-art
solver, the Succinct Solver and show our solver is at least 10-times faster than the Succinct Solver. On some benchmarks linearity is reached by the use of unification. Although the result of unification is often imprecise, a heuristic study is conducted to detect where the loss of precision may happen. We apply the heuristics on benchmarks and achieve not only efficient but also
precise analysis. |
| Keywords | inclusion constraint, unification, program analysis |
| Type | Conference paper [With referee] |
| Conference | The 17th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR'07) |
| Editors | Andy King |
| Year | 2008 Vol. LNCS No. 4915 pp. 121-136 |
| Publisher | Springer-verlag |
| Series | Lecture Notes in Computer Science |
| BibTeX data | [bibtex] |
| IMM Group(s) | Computer Science & Engineering |