CAREER: The Automata Theoretic Method in Software Verification

提案编号：0747041标题：软件验证中的自动机理论方法PI：Madhusudan Parthasarathy正确的程序很难编写。自动可靠地发现错误的工具对于确保正确的软件工程是必不可少的。 自动机理论在硬件验证中有很大的影响，它形成了针对时序逻辑的模型检查系统的基础。该项目将自动机理论方法应用于软件验证领域。 自动机理论为软件验证提供了几种全新的机制，包括处理递归和并发的复杂控制流，以及将逻辑规范连接到验证算法。该项目将开发这些机制，并将其应用于解决以下软件验证领域的关键问题：-开发用于指定递归程序的复杂事件序列属性的时态逻辑;- 使用自动机监察系统，检查并发程式是否违反原子性;及-使用新的自动机抽象系统，检查处理动态资料的程式的堆特性。此外，我们亦会发展两种工具：一个监视并发程序的原子性违反，第二个实现一个抽象框架来验证堆密集型程序。 开发的技术将为分析软件的基本问题铺平创新的道路。这些技术将对软件行业中构建和使用的分析工具产生直接影响，并显着推进软件验证的前景。

Proposal Number: 0747041TITLE: The Automata Theoretic Method in Software VerificationPI: Madhusudan ParthasarathyCorrect programs are hard to write. Tools that find errors automatically and reliably are essential to ensure engineering of correct software. Automata theory has had a great impact in hardware verification, where it forms the basis of model-checking systems against temporal logics. This project leverages automata-theoretic methods to the field of software verification. Automata theory provides several strikingly new mechanisms for verifying software, including handling of complex control flows of recursion and concurrency, and bridging logical specifications to verification algorithms.The project will develop these mechanisms and apply them to solve key problems in the following areas of software verification:- Developing temporal logics for specifying complex event sequence properties of recursive programs;- Checking atomicity violations in concurrent programs using automata-based monitoring; and- Verifying heap properties of programs manipulating dynamic data, using a novel automata based abstraction.In addition, two tools will be developed: one monitors concurrent programs for atomicity violations, and the second implements an abstraction framework to verify heap-intensive programs. The techniques developed will pave innovative pathways into the fundamental problems of analyzing software. The techniques will have immediate impact on analysis tools built and used in the software industry, and significantly advance the landscape of software verification.