Tìm kiếm

Tiêu chí lọc:

Tiêu chí lọc:

Tác giả

Chủ đề

Năm xuất bản

Toàn văn

Kết quả tìm kiếm

Hiện thị kết quả từ 1 đến 2 của 2
  • <<
  • 1
  • >>
    • Improving AMULET2 for verifying multiplier circuits using SAT solving and computer algebra
    Tác giả : Daniela, Kaufmann; Armin, Biere;  Người hướng dẫn: -;  Đồng tác giả: - (2023)

    Verifying arithmetic circuits and most prominently multiplier circuits is an important problem which in practice is still considered to be challenging. One of the currently most successful verification techniques relies on algebraic reasoning. In this article, we present AMULET2, a fully automatic tool for verification of integer multipliers combining SAT solving and computer algebra. Our tool models multipliers given as and-inverter graphs as a set of polynomials and applies preprocessing techniques based on elimination theory of Gröbner bases.
    • Verified Propagation Redundancy and Compositional UNSAT Checking in CakeML
    Tác giả : Yong Kiam, Tan; Marijn J. H., Heule; Magnus O., Myreen;  Người hướng dẫn: -;  Đồng tác giả: - (2023)

    Modern SAT solvers can emit independently-checkable proof certificates to validate their results. The state-of-the-art proof system that allows for compact proof certificates is propagation redundancy (PR ). However, the only existing method to validate proofs in this system with a formally verified tool requires a transformation to a weaker proof system, which can result in a significant blowup in the size of the proof and increased proof validation time. This article describes the first approach to formally verify PR proofs on a succinct representation. We present (i) a new Linear PR (LPR) proof format, (ii) an extension of the DPR-trim tool to efficiently convert PR proofs into LPR format, and (iii) cake_lpr, a verified LPR proof checker developed in CakeML.