CAREER: Semantics-based Program Analysis via Symbolic Composition of Transfer Relations

9702805该项目研究在程序实际执行之前自动确定计算机程序的运行时行为的属性的任务。优化编译器长期以来一直致力于这一领域的研究，即通常所说的静态程序分析。最近，人们对在软件投入使用之前使用程序分析来验证其正确性或安全属性感兴趣。然而，由于存在类似于累积舍入误差的累积不精确现象，以及在存在循环和递归的情况下不变性质的不足，在实践中很难实现有用和准确的程序分析。这个项目考察了一种新的程序分析方法，旨在解决这些问题。这种方法的独特之处在于，它不分析执行状态，而是分析这些状态之间的变化，称为传输关系，从而能够分析以前未解决的编程构造，如一类函数、并发性、指针和引用、赋值、可变数据结构和数组。这项研究调查了这些分析在紧急问题上的应用，如确保不可信外来代码的安全和提高大型软件系统的可靠性。该项目将这项研究应用于一项教育计划，包括课程开发、对硕士学生的指导，以及关于计划分析的年度暑期学校的发展，包括一份新的文本。***

9702805 This project investigates the task of automatically determining properties of the run-time behavior of computer programs before the programs are actually executed. Optimizing compilers have long motivated research in this area, commonly known as static program analysis. More recently, there has been interest in using program analysis to verify correctness or safety properties of software before it is put into service. However, due both to the phenomenon of accumulated imprecision, which is akin to accumulated rounding error, and to the inadequacy of invariant properties in the presence of loops and recursion, useful and accurate program analysis is hard to achieve in practice. This project examines a new methodology for program analysis designed to address these problems. This methodology is distinctive in that it does not analyze execution states, but instead analyzes the changes, called transfer relations, between those states, thus enabling previously unsolved analyses of programming constructs such as first-class functions, concurrency, pointers and references, assignment, mutable data structures, and arrays. The research investigates the application of these analyses to urgent issues such as ensuring safety of untrusted foreign code and increasing reliability of large software systems. The project applies this research to an educational plan including course development, mentoring of masters students, and the development of an annual summer school on program analysis, including a new text. ***