Show simple item record

dc.contributor.authorPoetzsch-Heffter, Arnden_US
dc.description.abstractThis 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.en_US
dc.format.extent2241511 bytes
dc.format.extent511252 bytes
dc.publisherCornell Universityen_US
dc.subjectcomputer scienceen_US
dc.subjecttechnical reporten_US
dc.titleInterprocedural Data Flow Analysis Based on Temporal Specificationsen_US
dc.typetechnical reporten_US

Files in this item


This item appears in the following Collection(s)

Show simple item record