University of Minnesota
Software Engineering Center

You are here

David Lacey

Recent Publications

Compiler Optimization Correctness by Temporal Logic

Rewrite rules with side conditions can elegantly express many classical compiler optimizations for imperative programming languages. In this paper, programs are written in an intermediate language and transformation-enabling side conditions are specified in a temporal logic suitable for describing program data flow.

Universal Regular Path Queries

Given are a directed edge-labelled graph G with a distinguished node n0, and a regular expression P which may contain variables. We wish to compute all substitutions phi (of symbols for variables), together with all nodes n such that all paths n0 to n are in phi(P). We derive an algorithm for this problem using relational algebra, and show how it may be implemented in Prolog. The motivation for the problem derives from a declarative framework for specifying compiler optimisations.

Proving Correctness of Compiler Optimizations by Temporal Logic

Many classical compiler optimizations can be elegantly expressed using rewrite rules of form: II' if φ, where I, I' are intermediate language instructions and φ is a property expressed in a temporal logic suitable for describing program data flow. Its reading: If the current program π contains an instruction of form I at some control point p, and if flow condition φ is satisfied at p, then replace I by I'.