权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

SHF : Small: Certified Automated Reasoning with BDDs (CARB)

SHF：小型：经过 BDD 认证的自动推理 (CARB)

基本信息

批准号：
2108521
负责人：
Marienus Heule
金额：
$ 49.97万
依托单位：
Carnegie-Mellon University
依托单位国家：
美国
项目类别：
Standard Grant
财政年份：
2021
资助国家：
美国
起止时间：
2021-06-01 至 2024-05-31
项目状态：
已结题

来源：
https://www.nsf.gov/awardsearch/showAward?AWD_ID=2108521&HistoricalAwards=false
关键词：
SHF Small Certified Automated Reasoning

项目摘要

Automated reasoning programs allow computers to apply methods based on mathematical logic to evaluate the correctness and security of hardware and software. They overcome the limitations of human reasoning with greater capacity, rigor, and reliability. Unfortunately, like all complex software systems, these programs may contain errors in the core algorithms or their implementations, causing them to produce incorrect results. This risk can be eliminated by having the program generate a checkable proof: a detailed account of its reasoning process in a formal, logical notation. This proof can then be checked by a much simpler checking program, quickly detecting any erroneous steps. This project extends the scope of automated reasoning programs for which checkable proofs can be generated, enabling more advanced forms of analysis to be performed in a trustworthy manner. Proof generation has become a common feature of Boolean satisfiability (SAT) solvers, greatly improving their reliability and trustworthiness. This project aims to improve the ability of other automated reasoning programs to generate checkable proofs of their results. It extends the proof rules used by existing logical frameworks to enable additional reasoning capabilities. Formally verified checkers that support these rules are implemented and made available. In terms of automated reasoning, the project devises new formulations of quantified Boolean formulas (QBF), dependency QBF (DQBF), model counting, and model checking that can generate proofs in existing and new logical frameworks. Reduced Ordered Binary Decisions Diagrams (BDDs) are used as the underlying mechanism for implementing the reasoning programs. BDDs have a proven track record for solving the problems of interest, and the reasoning behind many underlying algorithms can readily be expressed in simple logical frameworks. Preliminary work on proof generation by a BDD-based SAT solver demonstrate that other automated reasoning tasks are amenable to this approach.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.

自动推理程序允许计算机应用基于数学逻辑的方法来评估硬件和软件的正确性和安全性。它们以更大的能力、严谨性和可靠性克服了人类推理的局限性。不幸的是，像所有复杂的软件系统一样，这些程序可能在核心算法或其实现中包含错误，导致它们产生不正确的结果。这种风险可以通过让程序生成可检查的证明来消除：用正式的逻辑符号详细说明其推理过程。然后可以用一个简单得多的检查程序来检查这个证明，快速检测出任何错误步骤。该项目扩展了自动推理程序的范围，可以为其生成可检查的证明，使更高级的分析形式能够以可信的方式执行。证明生成已成为布尔可满足性（SAT）求解器的共同特征，极大地提高了其可靠性和可信度。该项目旨在提高其他自动推理程序的能力，以生成其结果的可检查证明。它扩展了现有逻辑框架所使用的证明规则，以支持额外的推理能力。已实现并提供支持这些规则的经过正式验证的检查器。在自动推理方面，该项目设计了量化布尔公式（QBF）、依赖性QBF （DQBF）、模型计数和模型检查的新公式，这些公式可以在现有的和新的逻辑框架中生成证明。简化有序二进制决策图（bdd）被用作实现推理程序的底层机制。bdd在解决感兴趣的问题方面有良好的记录，并且许多底层算法背后的推理可以很容易地用简单的逻辑框架表示。基于bdd的SAT解算器证明生成的初步工作表明，其他自动推理任务也适用于这种方法。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

项目成果

期刊论文数量（8）

专著数量（0）

科研奖励数量（0）

会议论文数量（0）

专利数量（0）

Generating Extended Resolution Proofs with a BDD-Based SAT Solver

使用基于 BDD 的 SAT 求解器生成扩展分辨率证明

DOI：
10.1145/3595295
发表时间：
2023
期刊：
ACM Transactions on Computational Logic
影响因子：
0.5
作者：
Bryant, Randal E.;Heule, Marijn J.
通讯作者：
Heule, Marijn J.

Moving Definition Variables in Quantified Boolean Formulas

在量化布尔公式中移动定义变量

DOI：
10.1007/978-3-030-99524-9_26
发表时间：
2022
期刊：
Book cover International Conference on Tools and Algorithms for the Construction and Analysis of Systems
影响因子：
0
作者：
Reeves, Joseph E.;Heule, Marijn J.;Bryant, Randal E.
通讯作者：
Bryant, Randal E.

Certified Knowledge Compilation with Application to Verified Model Counting

认证知识编译及其应用于验证模型计数

DOI：
10.4230/lipics.sat.2023.6
发表时间：
2023
期刊：
26th International Conference on Theory and Applications of Satisfiability Testing
影响因子：
0
作者：
Bryant, Randal E.;Nawrocki, Wojciech;Avigad, Jeremy;Heule, Marijn J.
通讯作者：
Heule, Marijn J.

Clausal Proofs for Pseudo-Boolean Reasoning

伪布尔推理的子句证明

DOI：
10.1007/978-3-030-99524-9_25
发表时间：
2022
期刊：
International Conference on Tools and Algorithms for the Construction and Analysis of Systems
影响因子：
0
作者：
Bryant, Randal E.;Heule, Marijn J.
通讯作者：
Heule, Marijn J.

Tbuddy: A Proof-Generating BDD Package