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.)