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.