CAREER: The Automata Theoretic Method in Software Verification

职业：软件验证中的自动机理论方法

• 批准号: 0747041
• 负责人: Madhusudan Parthasarathy
• 金额: $ 40万
• 依托单位: University of Illinois at Urbana-Champaign
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2008
• 资助国家: 美国
• 起止时间: 2008-06-15 至 2014-05-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0747041&HistoricalAwards=false
• 关键词: CAREER; Automata; Theoretic; Method; Software

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.

题目：软件验证中的自动机理论方法pi: Madhusudan parthasarathy正确的程序很难编写。自动、可靠地发现错误的工具对于确保正确的软件工程至关重要。自动机理论对硬件验证有很大的影响，它构成了针对时间逻辑的模型检查系统的基础。本项目将自动机理论方法应用于软件验证领域。自动机理论为验证软件提供了几个引人注目的新机制，包括处理递归和并发的复杂控制流，以及将逻辑规范连接到验证算法。该项目将开发这些机制，并将其应用于解决以下软件验证领域的关键问题：-开发用于指定递归程序的复杂事件序列属性的时间逻辑；-使用基于自动机的监控检查并发程序中的原子性违规；-使用一种新的基于自动机的抽象来验证操作动态数据的程序的堆属性。此外，还将开发两个工具：一个监视并发程序是否违反原子性，另一个实现一个抽象框架来验证堆密集型程序。所开发的技术将为分析软件的基本问题铺平创新的道路。这些技术将对软件行业中构建和使用的分析工具产生直接的影响，并显著地推进软件验证的前景。