In program analysis, the collecting semantics of a program associates with each "program point" the set of program states attainable when control reaches that point during all possible runs of the program on a given set of input data. An important problem in static analysis is to compute over-approximations of the collecting semantics, which has many potential applications, include optimizing compilation, strictness analysis, program transformation, and partial evaluation.

This project concerns an approach to over-approximating the collecting semantics of functional programs introduced by Jones and Andersen (2007). Functional programs (such as those of Haskell) are systematically translated to equivalent term rewriting systems by a process of lambda-lifting. Given a set of program inputs, a simple algorithm is given that constructs a regular tree grammar which is a representation of the over-approximation of the corresponding collecting semantics.

The goal is to implement Jones and Andersen's algorithm, with a view to applying it to the flow analysis of Haskell programs.

Relevant courses