Efficient verified (UN)SAT certificate checking

DOI10.1007/s10817-019-09525-zzbMath1468.68134OpenAlexW2944421753WikidataQ127780288 ScholiaQ127780288MaRDI QIDQ5919480

Peter Lammich

Publication date: 3 March 2020

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-019-09525-z

zbMATH Keywords

stepwise refinementformal verificationSAT solvingIsabelle/HOLDRATUNSAT certificatesverified software

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (6)

A proof system for graph (non)-isomorphism verification ⋮ Generating Extended Resolution Proofs with a BDD-Based SAT Solver ⋮ Never trust your solver: certification for SAT and QBF ⋮ \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML ⋮ Unnamed Item ⋮ Generating extended resolution proofs with a BDD-based SAT solver

Uses Software

• Coq
• Isabelle
• Isabelle/HOL
• Chaff
• LCF
• versat
• CakeML
• Autoref
• DRAT-trim
• GRAT
• GitHub
• Edmonds-Karp
• CAVA LTL Modelchecker
• Gabow SCC

Cites Work

• Unnamed Item
• Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL
• Formal verification of an executable LTL model checker with partial order reduction
• Isabelle/HOL. A proof assistant for higher-order logic
• Efficient, verified checking of propositional proofs
• A verified compiler from Isabelle/HOL to CakeML
• Verified model checking of timed automata
• Efficient certified RAT verification
• Formalizing the Edmonds-Karp Algorithm
• Proof-producing translation of higher-order logic into pure and stateful ML
• Verified Efficient Implementation of Gabow’s Strongly Connected Component Algorithm
• versat: A Verified Modern SAT Solver
• Applying Data Refinement for Monadic Programs to Hopcroft’s Algorithm
• Refinement to Imperative/HOL
• DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
• Extended Resolution Proofs for Conjoining BDDs
• Imperative Functional Programming with Isabelle/HOL
• Code Generation via Higher-Order Rewrite Systems
• Refinement Calculus
• Automatic Data Refinement
• Data Refinement in Isabelle/HOL
• Mechanical Verification of SAT Refutations with Extended Resolution
• CakeML
• Program development by stepwise refinement
• The Isabelle Collections Framework
• Efficient verified (UN)SAT certificate checking

This page was built for publication: Efficient verified (UN)SAT certificate checking