Verifying the conversion into CNF in dafny

DOI10.1007/978-3-030-88853-4_10OpenAlexW3202267117MaRDI QIDQ2148786FDOQ2148786

Ştefan Ciobâcă, Viorel Iordache

Publication date: 24 June 2022

Full work available at URL: https://doi.org/10.1007/978-3-030-88853-4_10

Mathematics Subject Classification ID

Logic in computer science (03B70)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Formalization and implementation of modern SAT solvers
• An optimality result for clause form translation
• Title not available (Why is that?)
• versat: A Verified Modern SAT Solver
• The Mechanical Verification of a DPLL-Based Satisfiability Solver
• A verified SAT solver framework with learn, forget, restart, and incrementality
• Formalization of Abstract State Transition Systems for SAT
• Extracting verified decision procedures: DPLL and Resolution
• Title not available (Why is that?)

Uses Software

• Coq
• Dafny
• Why3
• VCC
• versat
• GNATprove
• Archive Formal Proofs

This page was built for publication: Verifying the conversion into CNF in dafny

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