SwePub
Sök i LIBRIS databas

  Extended search

onr:"swepub:oai:research.chalmers.se:5e5dc370-e857-44de-9299-f5fab4aa0b1a"
 

Search: onr:"swepub:oai:research.chalmers.se:5e5dc370-e857-44de-9299-f5fab4aa0b1a" > Verified Propagatio...

  • 1 of 1
  • Previous record
  • Next record
  •    To hitlist

Verified Propagation Redundancy and Compositional UNSAT Checking in CakeML

Tan, Yong Kiam (author)
Carnegie Mellon University (CMU)
Heule, Marijn J.H. (author)
Carnegie Mellon University (CMU)
Myreen, Magnus, 1983 (author)
Chalmers tekniska högskola,Chalmers University of Technology
 (creator_code:org_t)
2023-02-27
2023
English.
In: International Journal on Software Tools for Technology Transfer. - : Springer Science and Business Media LLC. - 1433-2779 .- 1433-2787. ; 25:2, s. 167-184
  • Journal article (peer-reviewed)
Abstract Subject headings
Close  
  • 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. We also enhance these tools with (iv) a new compositional proof format designed to enable separate (parallel) proof checking. The LPR format is backwards compatible with the existing LRAT format, but extends LRAT with support for the addition of PR clauses. Moreover, cake_lpr is verified using CakeML ’s binary code extraction toolchain, which yields correctness guarantees for its machine code (binary) implementation. This further distinguishes our clausal proof checker from existing checkers because unverified extraction and compilation tools are removed from its trusted computing base. We experimentally show that: LPR provides efficiency gains over existing proof formats; cake_lpr ’s strong correctness guarantees are obtained without significant sacrifice in its performance; and the compositional proof format enables scalable parallel proof checking for large proofs.

Subject headings

TEKNIK OCH TEKNOLOGIER  -- Elektroteknik och elektronik -- Inbäddad systemteknik (hsv//swe)
ENGINEERING AND TECHNOLOGY  -- Electrical Engineering, Electronic Engineering, Information Engineering -- Embedded Systems (hsv//eng)
NATURVETENSKAP  -- Data- och informationsvetenskap -- Datavetenskap (hsv//swe)
NATURAL SCIENCES  -- Computer and Information Sciences -- Computer Sciences (hsv//eng)
TEKNIK OCH TEKNOLOGIER  -- Elektroteknik och elektronik -- Datorsystem (hsv//swe)
ENGINEERING AND TECHNOLOGY  -- Electrical Engineering, Electronic Engineering, Information Engineering -- Computer Systems (hsv//eng)

Keyword

compositional proof checking
linear propagation redundancy
binary code extraction

Publication and Content Type

art (subject category)
ref (subject category)

Find in a library

To the university's database

  • 1 of 1
  • Previous record
  • Next record
  •    To hitlist

Find more in SwePub

By the author/editor
Tan, Yong Kiam
Heule, Marijn J. ...
Myreen, Magnus, ...
About the subject
ENGINEERING AND TECHNOLOGY
ENGINEERING AND ...
and Electrical Engin ...
and Embedded Systems
NATURAL SCIENCES
NATURAL SCIENCES
and Computer and Inf ...
and Computer Science ...
ENGINEERING AND TECHNOLOGY
ENGINEERING AND ...
and Electrical Engin ...
and Computer Systems
Articles in the publication
International Jo ...
By the university
Chalmers University of Technology

Search outside SwePub

Kungliga biblioteket hanterar dina personuppgifter i enlighet med EU:s dataskyddsförordning (2018), GDPR. Läs mer om hur det funkar här.
Så här hanterar KB dina uppgifter vid användning av denna tjänst.

 
pil uppåt Close

Copy and save the link in order to return to this view