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

职业：通过传输关系的符号组合进行基于语义的程序分析

• 批准号: 9702805
• 负责人: Christopher Colby
• 金额: $ 20.06万
• 依托单位: Loyola University of Chicago
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 1997
• 资助国家: 美国
• 起止时间: 1997-08-15 至 2000-07-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9702805&HistoricalAwards=false
• 关键词: CAREER; Semantics; based; Program; Analysis

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

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