Efficient verified (UN)SAT certificate checking
From MaRDI portal
Publication:5919480
DOI10.1007/s10817-019-09525-zzbMath1468.68134OpenAlexW2944421753WikidataQ127780288 ScholiaQ127780288MaRDI QIDQ5919480
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
stepwise refinementformal verificationSAT solvingIsabelle/HOLDRATUNSAT certificatesverified software
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
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