Program Analysis

A popular path to obtain a program analysis is to present (and implement) the analysis as non-standard type inference, by marrying a type language with notation for decorating type expressions, the decorations expressing the program properties of interest.

I co-designed a generic framework for the constraint-based program analysis of functional programs with structured data where program properties are represented in terms of Boolean constraints. The framework can be seen as an instance of HM(X) where X is instantiated to the Boolean constraint domain. Specific applications include a binding-time [40], strictness [39] and exception analysis [36]. These analyses are available as part of the Glasgow Haskell Compiler GHC 4.2.

In another line of work on program analysis, I co-developed a novel resource-usage verification analysis [33] which employs a mixture of compile-time analysis and run-time testing to verify that a program conforms to a resource usage policy specified by a DFA which details allowed sequences of operations on resources.

Martin Sulzmann 2006-07-19