Interprocedural Data Flow Analysis Based on Temporal Specifications

Abstract

This paper investigates the specification of data flow problems by temporal logic formulas and proves fixpoint analyses correct. Temporal formulas are interpreted w.r.t. programming language semantics given in the framework of evolving algebras. This enables very high-level specifications, in particular for history sensitive problems. E.g. the classical bit vector analyses can be refined by using information about conditions in branches without having to change their specifications. The general semantics framework makes the approach directly applicable to realistic programming languages. We use the specifications to prove fixpoint implementations of data flow analyses correct. As an example, we develop a powerful interprocedural deadness analysis that uses constant information depending on the context where the active procedure was called. By proving such a combination of backward and forward analyses correct, we illustrate the use of specifications in correctness proofs.