\texttt{cake\_lpr}: verified propagation redundancy checking in CakeML
From MaRDI portal
Publication:2233509
DOI10.1007/978-3-030-72013-1_12zbMath1474.68194OpenAlexW3137055701MaRDI QIDQ2233509
Magnus O. Myreen, Marijn J. H. Heule, Yong Kiam Tan
Publication date: 18 October 2021
Full work available at URL: https://doi.org/10.1007/978-3-030-72013-1_12
Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items (5)
cake_lpr ⋮ Generating Extended Resolution Proofs with a BDD-Based SAT Solver ⋮ Preprocessing of propagation redundant clauses ⋮ Unnamed Item ⋮ Preprocessing of propagation redundant clauses
Uses Software
Cites Work
- Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL
- Computer-aided proof of Erdős discrepancy properties
- Efficient, verified checking of propositional proofs
- Software verification with ITPs should use binary code extraction to reduce the TCB (short paper)
- Extended resolution simulates \({\mathsf{DRAT}}\)
- A verified proof checker for higher-order logic
- Generating extended resolution proofs with a BDD-based SAT solver
- SMTCoq: a plug-in for integrating SMT solvers into Coq
- Strong extension-free proof systems
- Formally verifying the solution to the Boolean Pythagorean triples problem
- What a difference a variable makes
- Efficient certified RAT verification
- Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer
- Proof-producing translation of higher-order logic into pure and stateful ML
- versat: A Verified Modern SAT Solver
- Inprocessing Rules
- Verified Characteristic Formulae for CakeML
- A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
- DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
- A Brief Overview of HOL4
- The verified CakeML compiler backend
- Efficient verified (UN)SAT certificate checking
This page was built for publication: \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML
