skip to main content
US FlagAn official website of the United States government
dot gov icon
Official websites use .gov
A .gov website belongs to an official government organization in the United States.
https lock icon
Secure .gov websites use HTTPS
A lock ( lock ) or https:// means you've safely connected to the .gov website. Share sensitive information only on official, secure websites.

Explore Research Products in the PAR
It may take a few hours for recently added research products to appear in PAR search results.


Title: TBUDDY: A Proof-Generating BDD Package
The TBUDDY library enables the construction and manipulation of reduced, ordered binary decision diagrams (BDDs). It extends the capabilities of the BUDDY BDD pack- age to support trusted BDDs, where the generated BDDs are accompanied by proofs of their logical properties. These proofs are expressed in a standard clausal framework, for which a variety of proof checkers are available. Building on TBUDDY via its application-program interface (API) enables developers to implement automated reasoning tools that generate correctness proofs for their outcomes. In some cases, BDDs serve as the core reasoning mechanism for the tool, while in other cases they provide a bridge from the core reasoner to proof generation. A Boolean satisfiability (SAT) solver based on TBUDDY achieves polynomial scaling when generating unsatisfiability proofs for a number of problems that yield exponentially-sized proofs with standard solvers. It performs particularly well for formulas containing parity constraints, where it can employ Gaussian elimination to systematically simplify the constraints.  more » « less
Award ID(s):
2108521
PAR ID:
10410349
Author(s) / Creator(s):
Editor(s):
Griggio, Alberto; Rungta, Neha
Date Published:
Journal Name:
Formal methods in computeraided design
Volume:
3
Issue:
1
ISSN:
2708-7824
Page Range / eLocation ID:
49-58
Format(s):
Medium: X
Sponsoring Org:
National Science Foundation
More Like this
  1. ; (, International Conference on Tools and Algorithms for the Construction and Analysis of Systems)
    Fisman, D.; Rosu, G. (Ed.)
    When augmented with a Pseudo-Boolean (PB) solver, a Boolean satisfiability (SAT) solver can apply apply powerful reasoning methods to determine when a set of parity or cardinality constraints, extracted from the clauses of the input formula, has no solution. By converting the intermediate constraints generated by the PB solver into ordered binary decision diagrams (BDDs), a proof-generating, BDD-based SAT solver can then produce a clausal proof that the input formula is unsatisfiable. Working together, the two solvers can generate proofs of unsatisfiability for problems that are intractable for other proof-generating SAT solvers. The PB solver can, at times, detect that the proof can exploit modular arithmetic to give smaller BDD representations and therefore shorter proofs. 
    more » « less
  2. ; ; ; (, TU Wien Academic Press)
    Narodytska, Nina; Rümmer, Philipp (Ed.)
    Clausal proofs, particularly those based on the deletion resolution asymmetric tautology (DRAT) proof system, are widely used by Boolean satisfiability solvers for expressing proofs of unsatisfiability. Their success stems from their simplicity and scalability. When solvers go beyond pure propositional reasoning, however, generating clausal proofs becomes more difficult. Solvers that employ pseudo-Boolean reasoning, including cutting-planes operations, can express proofs in the VeriPB proof system, but its adoption is not widespread. We introduce PBIP (Pseudo-Boolean Implication Proof), a framework that provides an intermediate representation between VeriPB and clausal proofs. We also introduce a toolchain comprising 1) a VeriPB-to-PBIP translator that performs proof trimming and optimization, and 2) a PBIP-to-LRAT translator that makes use of proof-generating operations on ordered binary decision diagrams (BDDs) to generate clausal proofs in LRAT format, a variant of the DRAT that allows efficient checking. We demonstrate the viability of our approach, the effectiveness of our trimming, and the performance of our clausal proof generator on a set of native PB benchmarks and compare our approach to direct checking of VeriPB proofs. 
    more » « less
  3. ; ; (, SIGCSE 2023: Proceedings of the 54th ACM Technical Symposium on Computer Science Education)
    Rigorous, mathematical reasoning, i.e., proof, is the foundation of any undergraduate computer science education. However, students find mathematical proof exceedingly challenging, but also at the same time do not see its relevance to programming. We address these concerns with Snowflake, an educational proof assistant designed to help undergraduates overcome these difficulties when authoring mathematical proof. Snowflake does this by operating in a context where mathematical proof is introduced alongside programming in either a CS1 or CS2 context. The lens that we use to unite the two concepts is program correctness, a topic that immediately makes relevant the concept of formal reasoning as students are perpetually faced with the issue of whether their code is correct. Snowflake is a proof assistant designed for the needs of undergraduates in courses that closely time programming and proof. It is a web-based application that helps students author proofs not only in the context of program correctness in-the-small, but also other topics found in discrete mathematics courses. We report on the design of Snowflake, the kinds of reasoning it enables, and our plans to deploy Snowflake in the classroom. 
    more » « less
  4. ; ; (, Springer Nature Switzerland)
    Abstract This paper presents , a new intermediate verification language and deductive verification tool that provides inbuilt support for concurrency reasoning. ’s meta-theory is based on the higher-order concurrent separation logic Iris, incorporating core features such as user-definable ghost state and thread-modular reasoning via shared-state invariants. To achieve better accessibility and enable proof automation via SMT solvers, restricts Iris to its first-order fragment. The entailed loss of expressivity is mitigated by a higher-order module system that enables proof modularization and reuse. We provide an overview of the language and describe key aspects of the supported proof automation. We evaluate on a benchmark suite of verification tasks comprising linearizability and memory safety proofs for common concurrent data structures and clients as well as one larger case study. Our evaluation shows that improves over existing proof automation tools for Iris in terms of verification times and usability. Moreover, the tool significantly reduces the proof overhead compared to proofs constructed using the Iris/Rocq proof mode. 
    more » « less
  5. ; (, Tools and Algorithms for the Construction and Analysis of Systems)
    Groote, J. F.; Larsen, K. G. (Ed.)
    In 2006, Biere, Jussila, and Sinz made the key observation that the underlying logic behind algorithms for constructing Reduced, Ordered Binary Decision Diagrams (BDDs) can be encoded as steps in a proof in the extended resolution logical framework. Through this, a BDD-based Boolean satisfiability (SAT) solver can generate a checkable proof of unsatisfiability. Such proofs indicate that the formula is truly unsatisfiable without requiring the user to trust the BDD package or the SAT solver built on top of it. We extend their work to enable arbitrary existential quantification of the formula variables, a critical capability for BDD-based SAT solvers. We demonstrate the utility of this approach by applying a prototype solver to obtain polynomially sized proofs on benchmarks for the mutilated chessboard and pigeonhole problems—ones that are very challenging for search-based SAT solvers. 
    more » « less
  • Citation Formats
  • MLA
  • APA
  • Chicago
  • BibTeX
  • Save / Share this Record
  • Send to Email