Constraint-based Static Analysis of Programs
Henny Sipma (Stanford University)
- Place: E2, Rm 392
- Time: 2-3:10pm, Wednesday, March 15, 2006
Abstract
We present a constraint-based approach to static analysis of programs. The approach involves the following steps: (1) Fix a template property, that is, a property of a certain shape with unknown coefficients; (2) Provide the conditions for the property to hold; (3) Encode the conditions as a system of constraints using rules that allow computing consequences; (4) Solve the constraints; (5) Substitute the solutions in the template property; all concrete properties thus obtained are properties of the system of the desired kind. We demonstrate how this approach can be used to generate linear inequality invariants, linear ranking functions, and polynomial equality invariants.
The advantage of this approach is that it does not require widening. Controlling the complexity of the constraint system can be achieved by strengthening the conditions on the property or constraining the template property itself. Other advantages are that it can be used to generate any property that can be encoded as a system of constraints, and that it can generate properties in any domain that allows computation of consequences. A disadvantage of the approach is that the resulting system of constraints can have high complexity. Constraint solving, however, is a very active field of research, and any advances in this area directly improve scalability and precision of constraint-based program analysis.
Joint work with Michael Colon, Sriram Sankaranarayanan, Aaron Bradley, and Zohar Manna.