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

Internals

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

Comments

Links

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

Related papers

https://doi.org/10.1007/978-3-030-72013-1_12 (TACAS '21)

Last publication date

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.