Verified verifying: SMT-LIB for strings in Isabelle (Q6199876): Difference between revisions

@@ Property / cites work @@
+Flexible proof production in an industrial-strength SMT solver
+Normal rank
@@ Property / cites work @@
+Satisfiability Modulo Theories
@@ Property / cites work: Satisfiability Modulo Theories / rank @@
+Normal rank
@@ Property / cites work @@
+An SMT solver for regular expressions and linear arithmetic over string length
+Normal rank
@@ Property / cites work @@
+Path Feasibility Analysis for String-Manipulating Programs
+Normal rank
@@ Property / cites work @@
+A verified SAT solver framework with learn, forget, restart, and incrementality
+Normal rank
@@ Property / cites work @@
+A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality
+Normal rank
@@ Property / cites work @@
+Fast LCF-Style Proof Reconstruction for Z3
@@ Property / cites work: Fast LCF-Style Proof Reconstruction for Z3 / rank @@
+Normal rank
@@ Property / cites work @@
+Derivatives of Regular Expressions
@@ Property / cites work: Derivatives of Regular Expressions / rank @@
+Normal rank
@@ Property / cites work @@
+On solving word equations using SAT
@@ Property / cites work: On solving word equations using SAT / rank @@
+Normal rank
@@ Property / cites work @@
+Formalization of Basic Combinatorics on Words
@@ Property / cites work: Formalization of Basic Combinatorics on Words / rank @@
+Normal rank
@@ Property / cites work @@
+Proof Pearl: regular expression equivalence and relation algebra
+Normal rank
@@ Property / cites work @@
+Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL
+Normal rank
@@ Property / cites work @@
+Formalization of Abstract State Transition Systems for SAT
+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 @@
+The Mechanical Verification of a DPLL-Based Satisfiability Solver
+Normal rank
@@ Property / cites work @@
+The Isabelle Framework
@@ Property / cites work: The Isabelle Framework / rank @@
+Normal rank
@@ Property / cites work @@
+Automata-based symbolic string analysis for vulnerability detection
+Normal rank