Fast and verified UNSAT certificate checking

DOI10.1007/978-3-031-63498-7_26MaRDI QIDQ7034849zbMATH OpenFDO

Authors Peter Lammich

Publication date 31 January 2025

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-63498-7_26

zbMATH Keywords

Isabelle-LLVMLRATUNSAT certificatesverified software

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML
• A flexible proof format for SAT solver-elaborator communication
• Applying data refinement for monadic programs to Hopcroft's algorithm
• Certified dominance and symmetry breaking for combinatorial optimisation
• 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
• Faster LRAT checking than solving with CaDiCaL
• scientific article; zbMATH DE number 7649971 (Why is no real title available?)
• Refinement to Imperative/HOL
• TRX: a formally verified parser interpreter
• Validating LR(1) Parsers

Cited in

(2)

• Improving the SMT proof reconstruction pipeline in Isabelle/HOL
• Verifying an efficient algorithm for computing Bernoulli numbers

This page was built for publication: Fast and verified UNSAT certificate checking

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q7034849)