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

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

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.