CAREER: Advanced Decision Procedures forWords, Trees and Lists

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

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.