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.