Research Initiation Award: Formal and Contextual Analysis of Software

点击翻译按钮获取中文摘要

9308726 Jackson Many of the tasks demanded by evolving software-maintenance, reverse engineering, restructuring, etc.-depend on analysis. Large programs confound any attempt at hand analysis, so research has focused on tools that analyze programs automatically. Broadly speaking, two kinds of tools have been proposed: knowledge-based tools that can associate properties of program components with notions from the problem domain, and compilerlike tools that determine relationships among components by calculating dependencies, slices, module hierarchies, etc. Each approach has disadvantages. The knowledge-based tools, because they only associate problem domain notions with components informally, cannot provide rigorous analysis; answers to queries tend to be more like hints than sound inferences. The compiler-like tools are confined to low- level analysis of the code, so the queries, and their responses, must be formulated in terms of code constructs alone. This work combines some of the advantages of both approaches. The key idea is contextual abstraction. The user specifies an abstraction relationship between program components and problem domain notions. A variety of analyses then becomes possible by interpreting properties of the code in problem domain terms. And because the abstraction relationship is formal, the analyses are rigorous and can include, for example, partial verification. ***