CAREER: Advanced Decision Procedures forWords, Trees and Lists

职业：单词、树和列表的高级决策程序

• 批准号: 0954132
• 负责人: Gianfranco Ciardo
• 金额: $ 49.96万
• 依托单位: Iowa State University
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2010
• 资助国家: 美国
• 起止时间: 2010-03-15 至 2017-02-28
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0954132&HistoricalAwards=false
• 关键词: CAREER; Advanced; Decision; Procedures; forWords

As complex computer systems become ever more pervasive in our society, especially with the increasing deployment of multi-core processors and clusters of servers in the nation's cyber infrastructure, the demand to advance techniques on program analysis and verification has ever been more intensive. Logic-based reasoning techniques have played a fundamental role in assurance of correctness, reliability and security of computer systems. These techniques divide into two categories: general-purpose theorem proving and specialized decision algorithms. Theorem provers, enjoying a high degree of inference completeness, can prove sophisticated properties but require human guidance in general. On the other hand, decision algorithms, though confined within specialized domains, can automatically discharge a large amount of constraints. It has long been a challenge to combine the merits of the two kinds of techniques to produce a new generation of analysis tools that can handle a wide range of constraints with a high degree of automation. This research is to answer this challenge by building powerful decision theories as well as practical tools for reasoning about high-level data structures that are widely used in advanced programming languages and algorithms. The results would have wide and immediate applications in system analysis, improving the precision and scope of static and runtime analysis techniques.

随着复杂的计算机系统在我们的社会中变得越来越普遍，特别是在国家网络基础设施中越来越多地部署多核处理器和服务器集群，对程序分析和验证技术的需求也越来越强烈。基于逻辑的推理技术在保证计算机系统的正确性、可靠性和安全性方面发挥了重要作用。这些技术分为两类：通用定理证明和专用决策算法。定理证明者享有高度的推理完备性，可以证明复杂的性质，但通常需要人类的指导。另一方面，决策算法虽然局限于特定的领域，但可以自动释放大量的约束。长期以来，结合这两种技术的优点来产生新一代的分析工具一直是一个挑战，这些分析工具能够以高度自动化的方式处理广泛的约束。本研究旨在通过构建强大的决策理论和实用工具来回答这一挑战，这些工具用于推断高级编程语言和算法中广泛使用的高级数据结构。结果将在系统分析中有广泛和直接的应用，提高静态和运行时分析技术的精度和范围。