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 , strictness  and exception analysis . 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  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.