Finite Differencing of Logical Formulas for Static Analysis
Thomas Reps and 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.)