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求解器在证明生成方面的初步工作表明，其他自动推理任务也可以接受这种方法。该奖项反映了NSF的法定任务，并被认为是通过基金会的知识分子优点和更广泛影响的评估评估来评估的审查标准。

项目成果

期刊论文数量（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