Verified verifying: SMT-LIB for strings in Isabelle

DOI10.1007/978-3-031-40247-0_15MaRDI QIDQ6199876zbMATH OpenOpenAlexFDO

Authors Kevin Lotz, Mitja Kulczynski, Dirk Nowotka, Danny Bøgsted Poulsen, Anders Schlichtkrull

Publication date 28 February 2024

Published in Implementation and Application of Automata (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-031-40247-0_15

Mathematics Subject Classification ID

Formal languages and automata (68Q45)

Cites work

• A verified SAT solver framework with learn, forget, restart, and incrementality
• A verified SAT solver framework with learn, forget, restart, and incrementality
• An SMT solver for regular expressions and linear arithmetic over string length
• Automata-based symbolic string analysis for vulnerability detection
• Derivatives of Regular Expressions
• Fast LCF-Style Proof Reconstruction for Z3
• Flexible proof production in an industrial-strength SMT solver
• Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL
• Formalization of Abstract State Transition Systems for SAT
• Formalization of Basic Combinatorics on Words
• Isabelle/HOL. A proof assistant for higher-order logic
• On solving word equations using SAT
• Path Feasibility Analysis for String-Manipulating Programs
• Proof Pearl: regular expression equivalence and relation algebra
• Satisfiability modulo theories
• Solving String Theories Involving Regular Membership Predicates Using SAT
• The Isabelle Framework
• The mechanical verification of a DPLL-based satisfiability solver
• versat: A Verified Modern SAT Solver

This page was built for publication: Verified verifying: SMT-LIB for strings in Isabelle

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