Solving Weighted Constraints with Applications to Program Analysis

Research area: Program Analysis and VerificationSystems 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