\texttt{cake\_lpr}: verified propagation redundancy checking in CakeML
From MaRDI portal
Publication:2233509
Recommendations
Cites work
- A Brief Overview of HOL4
- A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
- A verified proof checker for higher-order logic
- Computer-aided proof of Erdős discrepancy properties
- DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
- Efficient certified RAT verification
- Efficient verified (UN)SAT certificate checking
- Efficient, verified checking of propositional proofs
- Extended resolution simulates \({\mathsf{DRAT}}\)
- Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL
- Formally verifying the solution to the Boolean Pythagorean triples problem
- Generating extended resolution proofs with a BDD-based SAT solver
- Inprocessing rules
- Proof-producing translation of higher-order logic into pure and stateful ML
- SMTCoq: a plug-in for integrating SMT solvers into Coq
- Software verification with ITPs should use binary code extraction to reduce the TCB (short paper)
- Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer
- Strong extension-free proof systems
- The verified CakeML compiler backend
- Verified characteristic formulae for CakeML
- versat: A Verified Modern SAT Solver
- What a difference a variable makes
Cited in
(20)- cake_lpr
- Preprocessing of propagation redundant clauses
- What a difference a variable makes
- Efficient certified RAT verification
- A flexible proof format for SAT solver-elaborator communication
- Efficient verified (UN)SAT certificate checking
- Efficient verified (UN)SAT certificate checking
- Preprocessing of propagation redundant clauses
- Generating Extended Resolution Proofs with a BDD-Based SAT Solver
- Certified dominance and symmetry breaking for combinatorial optimisation
- A More Pragmatic CDCL for IsaSAT and Targetting LLVM (Short Paper)
- Propositional proof skeletons
- Unsatisfiability proofs for distributed clause-sharing SAT solvers
- \textsc{Carcara}: an efficient proof checker and elaborator for SMT proofs in the Alethe format
- Incorporating a database of graphs into a proof assistant
- Practical algebraic calculus and Nullstellensatz with the checkers Pacheck and Pastèque and Nuss-Checker
- Clausal congruence closure
- Producing and verifying extremely large propositional refutations
- Producing proofs of unsatisfiability with distributed clause-sharing SAT solvers
- Fast and verified UNSAT certificate checking
This page was built for publication: \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2233509)
