Title:
Solving Weighted Constraints with Applications to Program Analysis
Solving Weighted Constraints with Applications to Program Analysis
Author(s)
Mangal, Ravi
Zhang, Xin
Naik, Mayur
Nori, Aditya
Zhang, Xin
Naik, Mayur
Nori, Aditya
Advisor(s)
Editor(s)
Collections
Supplementary to
Permanent Link
Abstract
Systems of weighted constraints are a natural formalism for many emerging tasks in program analysis and verification. Such systems
include both hard and soft constraints: the desired solution must satisfy
the hard constraints while optimizing the objectives expressed by the
soft constraints. Existing techniques for solving such constraint systems
sacrifice scalability or soundness by grounding the constraints eagerly,
rendering them unfit for program analysis applications. We present a lazy
grounding algorithm that generalizes and extends these techniques in a
unified framework. We also identify an instance of this framework that,
in the common case of computing the least solution of Horn constraints,
strikes a balance between the eager and lazy extremes by guiding the
grounding based on the logical structure of constraints. We show that our
algorithm achieves significant speedup over existing approaches without
sacrificing soundness for several real-world program analysis applications.
Sponsor
Date Issued
2015
Extent
Resource Type
Text
Resource Subtype
Technical Report