TC: EAGER: Collaborative Research: Parallel Automated Reasoning

国家计算基础设施的安全性对消费者信心、保护隐私、保护有价值的知识产权甚至国家安全都至关重要。基于逻辑的安全方法越来越受欢迎，部分原因是它们提供了一种精确的方法来描述和推理真实系统中的各种复杂性。也许更重要的是，可以使用自动推理技术来帮助用户驾驭这种复杂性。尽管自动推理前景光明，但它在实际应用中的应用仍然有限。其中一个主要原因是，对于许多问题，自动推理方法不够快，特别是在交互式环境中使用时（例如桌面计算中的浏览器插件，或在智能手机和pda上运行的移动应用程序）。该项目旨在通过研究新的设计和算法来解决自动推理的性能弱点，这些设计和算法具有利用并行性的统一主题。该项目将集中在自动演绎的三个主要领域：布尔可满足性、一阶推理和可满足性模理论。

The security of the national computing infrastructure is critical for consumer confidence, protection of privacy, protection of valuable intellectual property, and even national security. Logic-based approaches to security have been gaining popularity, in part because they provide a precise way to describe and reason about the kinds of complexity found in real systems. Perhaps even more importantly, automated reasoning techniques can be used to assist users in navigating this complexity. Despite the promise of automated reasoning, its use in practical applications is still limited. One of the primary reasons for this is that for many problems, automated reasoning methods are not fast enough, especially for use in interactive environments (such as browser plug-ins in desktop computing, or mobile applications running on smart phones and PDAs). This project aims to address the performance weakness of automated reasoning by investigating novel designs and algorithms with the unifying theme of exploiting parallelism. The project will focus on three main areas of automated deduction: Boolean satisfiability, first-order reasoning, and satisfiability modulo theories.