Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL (Q606999): Difference between revisions

@@ Property / describes a project that uses @@
+Archive Formal Proofs
@@ Property / describes a project that uses: Archive Formal Proofs / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Chaff
@@ Property / describes a project that uses: Chaff / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+BerkMin
@@ Property / describes a project that uses: BerkMin / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1016/j.tcs.2010.09.014
+Normal rank
@@ Property / OpenAlex ID @@
+W1991066194
@@ Property / OpenAlex ID: W1991066194 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5503674
@@ Property / cites work: Q5503674 / rank @@
+Normal rank
@@ Property / cites work @@
+Imperative Functional Programming with Isabelle/HOL
+Normal rank
@@ Property / cites work @@
+The complexity of theorem-proving procedures
@@ Property / cites work: The complexity of theorem-proving procedures / rank @@
+Normal rank
@@ Property / cites work @@
+A machine program for theorem-proving
@@ Property / cites work: A machine program for theorem-proving / rank @@
+Normal rank
@@ Property / cites work @@
+A Computing Procedure for Quantification Theory
@@ Property / cites work: A Computing Procedure for Quantification Theory / rank @@
+Normal rank
@@ Property / cites work @@
+Theory and Applications of Satisfiability Testing
@@ Property / cites work: Theory and Applications of Satisfiability Testing / rank @@
+Normal rank
@@ Property / cites work @@
+Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL
+Normal rank
@@ Property / cites work @@
+Formalization and implementation of modern SAT solvers
+Normal rank
@@ Property / cites work @@
+Q3562927
@@ Property / cites work: Q3562927 / rank @@
+Normal rank
@@ Property / cites work @@
+GRASP: a search algorithm for propositional satisfiability
+Normal rank
@@ Property / cites work @@
+Solving SAT and SAT Modulo Theories
@@ Property / cites work: Solving SAT and SAT Modulo Theories / rank @@
+Normal rank
@@ Property / cites work @@
+Isabelle/HOL. A proof assistant for higher-order logic
+Normal rank
@@ Property / cites work @@
+Towards mechanical metamathematics
@@ Property / cites work: Towards mechanical metamathematics / rank @@
+Normal rank
@@ Property / cites work @@
+The Mechanical Verification of a DPLL-Based Satisfiability Solver
+Normal rank
@@ Property / cites work @@
+SATO: An efficient propositional prover
@@ Property / cites work: SATO: An efficient propositional prover / rank @@
+Normal rank