a framework for construction and evaluation of high-level specifications for program analysis techniques
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.
evaluation program analysis formal specification reasoning implementation complexity understandability research language definition  framework 