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. ***