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

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.