Semantic Analysis and its Applications to Software Development

语义分析是对程序的自动分析，用于预测它们的运行时行为。这种分析因确定程序的语义属性的固有困难而变得复杂。现有的语义分析方法，如数据流分析、依赖分析等，都是通过寻找相对较弱的语义信息来解决这一问题的。虽然这些方法是有效和有用的，但它们存在两个缺点。首先，许多人没有得到严格的辩护。第二个缺点是它们提供的语义信息薄弱。为了纠正这些缺陷，本项目将研究(1)基于分析路径可执行性条件和形式规范和证明的新的语义分析方法的开发；(2)语义分析的新应用的开发；以及(3)演示新的语义分析方法和应用的原型系统的开发。

Semantic analysis is automated analysis of programs, used to predict their runtime behavior. Such analysis is complicated by the inherent difficulty of determining semantic properties of programs. Existing semantic analysis methods, such as data flow analysis and dependence analysis, deal with this problem by seeking relatively weak semantic information. While these methods are efficient and useful, they suffer from two drawbacks. First, many have not been justified rigorously. The second drawback is the weakness of the semantic information they provide. To rectify these drawbacks, this project will investigate (1) the development of new semantic analysis methods based on analyzing path executability conditions and formal specifications and proofs; (2) the development of new applications of semantic analysis; and (3) the development of prototype systems to demonstrate new semantic analysis methods and applications.