Abstract

Program analyses have traditionally been formulated as point solutions to specific program analysis problems. We present a comprehensive, unified framework that places program analyses within an algebraic lattice structure based on the program traces that each analysis identifies. In this framework each program analysis is characterized by the set of program traces that it identifies, with program analyses ordered by reverse subset inclusion over sets of identified program traces. With this order, the collection of program analyses comprises a lattice with least upper bound and greatest lower bound.

Download Publication