BROWSE

Author Profile

Browsing by Author Magnus O., Myreen

Jump to: 0-9 A B C D E F G H I J K L M N O P Q R S T U V W X Y Z
or enter first few letters:  
Showing results [1 - 1] / 1
    • Verified Propagation Redundancy and Compositional UNSAT Checking in CakeML
    Authors: Yong Kiam, Tan; Marijn J. H., Heule; Magnus O., Myreen;  Advisor: -;  Co-Author: - (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 int...