A verified SAT solver framework with learn, forget, restart, and incrementality
From MaRDI portal
(Redirected from Publication:1663234)
Recommendations
- A verified SAT solver framework with learn, forget, restart, and incrementality
- SAT-Based Compositional Verification Using Lazy Learning
- versat: A Verified Modern SAT Solver
- SAT-Based Scalable Formal Verification Solutions
- Formal verification of a generic framework to synthesize SAT-provers
- Assessing progress in SAT solvers through the Lens of incremental SAT
- Formalization and implementation of modern SAT solvers
Cites work
- scientific article; zbMATH DE number 1301853 (Why is no real title available?)
- scientific article; zbMATH DE number 5493266 (Why is no real title available?)
- A machine program for theorem-proving
- A verified SAT solver framework with learn, forget, restart, and incrementality
- AVATAR: The Architecture for First-Order Theorem Provers
- Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL
- Automated reasoning building blocks
- Automatic Data Refinement
- Automatic proof and disproof in Isabelle/HOL
- Code generation via higher-order rewrite systems
- Concrete semantics. With Isabelle/HOL
- Edinburgh LCF. A mechanized logic of computation
- Efficient certified RAT verification
- Efficient verified (UN)SAT certificate checking
- Extending Sledgehammer with SMT solvers
- Fast LCF-Style Proof Reconstruction for Z3
- Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL
- Formalization of Abstract State Transition Systems for SAT
- Formalization of the Resolution Calculus for First-Order Logic
- Imperative Functional Programming with Isabelle/HOL
- Isabelle/HOL. A proof assistant for higher-order logic
- Locales: a module system for mathematical theories
- Mechanizing the metatheory of Sledgehammer
- Metamathematics, Machines and Gödel's Proof
- Optimal speedup of Las Vegas algorithms
- Partial Recursive Functions in Higher-Order Logic
- Program development by stepwise refinement
- Refinement to Imperative/HOL
- Resolution theorem proving
- Semi-intelligible Isar proofs from machine-generated proofs
- Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
- Soundness and completeness proofs by coinductive methods
- Teaching semantics with a proof assistant: no more LSD trip proofs
- The mechanical verification of a DPLL-based satisfiability solver
- Theory and Applications of Satisfiability Testing
- versat: A Verified Modern SAT Solver
Cited in
(16)- Verifying a sequent calculus Prover for first-order logic with functions in Isabelle/HOL
- A verified SAT solver framework with learn, forget, restart, and incrementality
- On enumerating short projected models
- Automated deduction
- A More Pragmatic CDCL for IsaSAT and Targetting LLVM (Short Paper)
- An Isabelle/HOL Formalization of the SCL(FOL) Calculus
- Certifying emptiness of timed Büchi automata
- \textsc{Carcara}: an efficient proof checker and elaborator for SMT proofs in the Alethe format
- versat: A Verified Modern SAT Solver
- Formalizing Bachmair and Ganzinger's ordered resolution prover
- Verified verifying: SMT-LIB for strings in Isabelle
- Formal verification of a generic framework to synthesize SAT-provers
- scientific article; zbMATH DE number 7566059 (Why is no real title available?)
- Formalized proof systems for propositional logic
- Verifying the conversion into CNF in dafny
- Verified Decision Procedures for Modal Logics.
Describes a project that uses
Uses Software
This page was built for publication: A verified SAT solver framework with learn, forget, restart, and incrementality
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1663234)
