Formal verification of a generic framework to synthesize SAT-provers

DOI10.1007/BF03177742MaRDI QIDQ2583288zbMATH OpenFDO

Authors Jose Antonio Alonso, Francisco Jesús Martín-Mateos, María José Hidalgo, José Luis Ruiz-Reina

Publication date 16 January 2006

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

Full work available at URL https://doi.org/10.1007/BF03177742

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Verification in ACL2 of a generic framework to synthesize SAT-provers
• A verified SAT solver framework with learn, forget, restart, and incrementality
• Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL
• A verified SAT solver framework with learn, forget, restart, and incrementality
• The mechanical verification of a DPLL-based satisfiability solver

Cites work

• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving
• scientific article; zbMATH DE number 3976991 (Why is no real title available?)
• scientific article; zbMATH DE number 1113992 (Why is no real title available?)
• scientific article; zbMATH DE number 837700 (Why is no real title available?)
• scientific article; zbMATH DE number 3274715 (Why is no real title available?)
• Implementing the Davis-Putnam method
• Structured theory development for a mechanized logic
• Verification in ACL2 of a generic framework to synthesize SAT-provers

Cited in

(19)

• A verified SAT solver framework with learn, forget, restart, and incrementality
• A logic-algebraic tool for reasoning with knowledge-based systems
• Integration of formal proof into unified assurance cases with Isabelle/SACM
• Automating automated reasoning. The case of two generic automated reasoning tools
• Formally verified tableau-based reasoners for a description logic
• Linear templates of ACTL formulas with an application to SAT-based verification
• A verified SAT solver framework with learn, forget, restart, and incrementality
• Satallax: An Automatic Higher-Order Prover
• scientific article; zbMATH DE number 6708298 (Why is no real title available?)
• Verification in ACL2 of a generic framework to synthesize SAT-provers
• A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
• Formalization of Abstract State Transition Systems for SAT
• scientific article; zbMATH DE number 5718039 (Why is no real title available?)
• Conservative Retractions of Propositional Logic Theories by Means of Boolean Derivatives: Theoretical Foundations
• scientific article; zbMATH DE number 177271 (Why is no real title available?)
• Satisfiability Checking of Non-clausal Formulas Using General Matings
• A comprehensive framework for saturation theorem proving
• Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL
• An approach from answer set programming to decision making in a railway interlocking system

Describes a project that uses

Uses Software

• ACL2

This page was built for publication: Formal verification of a generic framework to synthesize SAT-provers

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