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.
