Finite Differencing of Logical Formulas for Static Analysis

Abstract. This paper concerns mechanisms for maintaining the value of an instrumentation predicate (a.k.a. derived predicate or view), defined via a logical formula over core predicates, in response to changes in the values of the core predicates. It presents an algorithm for transforming the instrumentation predicate’s defining formula into a predicate-maintenance formula that captures what the instrumentation predicate’s new value should be. This technique applies to program-analysis problems in which the semantics of statements is expressed using logical formulas that describe changes to corepredicate values, and provides a way to reflect those changes in the values of the instrumentation predicates.

• Type: Conference
• Year: 2003
• Where: ESOP
• Authors: Thomas W. Reps, Shmuel Sagiv, Alexey Loginov
• Keywords: Core Predicates, ESOP 2003, Instrumentation Predicates, Logical Formulas, Programming Languages