PV4 cake_lprtakes a proof and checks whether it satisfies linear propagation redundancy expectations

Application domain/field

Proof checking

Type of tool

Proof checker

Expected input

A proof in LPR (Linear Propagation Redundancy)

Expected output

SAT? or VERIFIED UNSAT or resource exhaustion error


Built on top of CakeML; HOL4 The same paper has a tool to convert PR to LPR



Repository: https://github.com/tanyongkiam/cake_lpr

Related papers

cake_lpr: Verified Propagation Redundancy Checking in CakeML (TACAS '21)

Last publication date

ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.