TC: EAGER: Collaborative Research: Parallel Automated Reasoning

TC：EAGER：协作研究：并行自动推理

• 批准号: 1049495
• 负责人: Clark Barrett
• 金额: $ 12.48万
• 依托单位: New York University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2010
• 资助国家: 美国
• 起止时间: 2010-09-01 至 2012-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1049495&HistoricalAwards=false
• 关键词: TC; EAGER; Collaborative; Research; Parallel

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.

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