Abstract
Interpretation introduced the notion of formal specification of program analyses. Denotational frameworks are convenient for reasoning about such specifications. However, implementation considerations make denotational specifications complex and hard to develop. We present a framework that facilitates the construction and understanding of denotational specifications for program analysis techniques. The framework is exemplified by specifications for program analysis techniques from the literature and from our own research. This approach allows program analysis techniques to be incorporated into automatically generated program synthesizers by including their specifications with the language definition.

This publication has 9 references indexed in Scilit: