Finite Differencing of Logical Formulas for Static Analysis

Thomas Reps, Mooly Sagiv, and Alexey Loginov

This paper concerns mechanisms for maintaining the value of an instrumentation relation (also known as a derived relation or view), defined via a logical formula over core relations, in response to changes in the values of the core relations. It presents an algorithm for transforming the instrumentation relation's defining formula into a relation-maintenance formula that captures what the instrumentation relation's new value should be.

The technique applies to program-analysis problems in which the semantics of statements is expressed using logical formulas that describe changes to core-relation values, and provides a way to reflect those changes in the values of the instrumentation relations.

(Click here to access the paper: PDF.)