Efficient verified (UN)SAT certificate checking (Q5919480): Difference between revisions

@@ Property / cites work @@
+Refinement Calculus
@@ Property / cites work: Refinement Calculus / rank @@
+Normal rank
@@ Property / cites work @@
+Formal verification of an executable LTL model checker with partial order reduction
+Normal rank
@@ Property / cites work @@
+Imperative Functional Programming with Isabelle/HOL
+Normal rank
@@ Property / cites work @@
+Efficient certified RAT verification
@@ Property / cites work: Efficient certified RAT verification / rank @@
+Normal rank
@@ Property / cites work @@
+Q4513619
@@ Property / cites work: Q4513619 / rank @@
+Normal rank
@@ Property / cites work @@
+Data Refinement in Isabelle/HOL
@@ Property / cites work: Data Refinement in Isabelle/HOL / rank @@
+Normal rank
@@ Property / cites work @@
+Code Generation via Higher-Order Rewrite Systems
@@ Property / cites work: Code Generation via Higher-Order Rewrite Systems / rank @@
+Normal rank
@@ Property / cites work @@
+Efficient, verified checking of propositional proofs
+Normal rank
@@ Property / cites work @@
+A verified compiler from Isabelle/HOL to CakeML
@@ Property / cites work: A verified compiler from Isabelle/HOL to CakeML / rank @@
+Normal rank
@@ Property / cites work @@
+CakeML
@@ Property / cites work: CakeML / rank @@
+Normal rank
@@ Property / cites work @@
+Automatic Data Refinement
@@ Property / cites work: Automatic Data Refinement / rank @@
+Normal rank
@@ Property / cites work @@
+Verified Efficient Implementation of Gabow’s Strongly Connected Component Algorithm
+Normal rank
@@ Property / cites work @@
+Refinement to Imperative/HOL
@@ Property / cites work: Refinement to Imperative/HOL / rank @@
+Normal rank
@@ Property / cites work @@
+Efficient verified (UN)SAT certificate checking
@@ Property / cites work: Efficient verified (UN)SAT certificate checking / rank @@
+Normal rank
@@ Property / cites work @@
+The Isabelle Collections Framework
@@ Property / cites work: The Isabelle Collections Framework / rank @@
+Normal rank
@@ Property / cites work @@
+Formalizing the Edmonds-Karp Algorithm
@@ Property / cites work: Formalizing the Edmonds-Karp Algorithm / rank @@
+Normal rank
@@ Property / cites work @@
+Applying Data Refinement for Monadic Programs to Hopcroft’s Algorithm
+Normal rank
@@ Property / cites work @@
+Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL
+Normal rank
@@ Property / cites work @@
+Proof-producing translation of higher-order logic into pure and stateful ML
+Normal rank
@@ Property / cites work @@
+Isabelle/HOL. A proof assistant for higher-order logic
+Normal rank
@@ Property / cites work @@
+versat: A Verified Modern SAT Solver
@@ Property / cites work: versat: A Verified Modern SAT Solver / rank @@
+Normal rank
@@ Property / cites work @@
+Extended Resolution Proofs for Conjoining BDDs
@@ Property / cites work: Extended Resolution Proofs for Conjoining BDDs / rank @@
+Normal rank
@@ Property / cites work @@
+Mechanical Verification of SAT Refutations with Extended Resolution
+Normal rank
@@ Property / cites work @@
+DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
+Normal rank
@@ Property / cites work @@
+Verified model checking of timed automata
@@ Property / cites work: Verified model checking of timed automata / rank @@
+Normal rank
@@ Property / cites work @@
+Program development by stepwise refinement
@@ Property / cites work: Program development by stepwise refinement / rank @@
+Normal rank