@CONFERENCE\{IMM2008-05634,
    author       = "Y. Zhang and F. Nielsen",
    title        = "A Scalable Inclusion Constraint Solver Using Unification",
    year         = "2008",
    keywords     = "inclusion constraint, unification, program analysis",
    pages        = "121-136",
    booktitle    = "The 17th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR'07)",
    volume       = "LNCS",
    series       = "Lecture Notes in Computer Science",
    editor       = "Andy King",
    publisher    = "Springer-verlag",
    organization = "",
    address      = "",
    url          = "http://www2.compute.dtu.dk/pubdb/pubs/5634-full.html",
    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."
}