**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 algorithm runs in time linear in the size of the defining formula.

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. It provides a way to obtain values of the instrumentation relations that reflect the changes in core-relation values produced by executing a given statement.

We present experimental evidence that our technique is an effective one: for a variety of benchmarks, the relation-maintenance formulas produced automatically using our approach yield the same precision as the best available hand-crafted ones.

(Click here to access the paper: PDF.)