A Scalable Inclusion Constraint Solver Using Unification

Ye Zhang, Flemming Nielsen

AbstractWe 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.
Keywordsinclusion constraint, unification, program analysis
TypeConference paper [With referee]
ConferenceThe 17th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR'07)
EditorsAndy King
Year2008    Vol. LNCS    No. 4915    pp. 121-136
PublisherSpringer-verlag
SeriesLecture Notes in Computer Science
BibTeX data [bibtex]
IMM Group(s)Computer Science & Engineering