Simple Relational Correctness Proofs for Static Analyses and Program Transformations

Nick Benton

To appear at Principles of Programming Languages (POPL04), Venice, Italy, January 14-16, 2004


We show how some classical static analyses for imperative programs, and the optimizing transformations which they enable, may be expressed and proved correct using elementary logical and denotational techniques. The key ingredients are an interpretation of program properties as relations, rather than predicates, and a realization that although some program analyses are described in terms of intensional properties, the associated transformations are actually enabled by more liberal extensional properties.

Server START Conference Manager
Update Time 19 Sep 2003 at 17:40:42
Start Conference Manager
Conference Systems