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