Verified verifying: SMT-LIB for strings in Isabelle
From MaRDI portal
Publication:6199876
DOI10.1007/978-3-031-40247-0_15OpenAlexW4385701414MaRDI QIDQ6199876FDOQ6199876
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
Cites Work
- The Isabelle Framework
- Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL
- Derivatives of Regular Expressions
- Isabelle/HOL. A proof assistant for higher-order logic
- Satisfiability modulo theories
- Fast LCF-Style Proof Reconstruction for Z3
- Proof Pearl: regular expression equivalence and relation algebra
- Path Feasibility Analysis for String-Manipulating Programs
- versat: A Verified Modern SAT Solver
- The mechanical verification of a DPLL-based satisfiability solver
- An SMT solver for regular expressions and linear arithmetic over string length
- On solving word equations using SAT
- A verified SAT solver framework with learn, forget, restart, and incrementality
- A verified SAT solver framework with learn, forget, restart, and incrementality
- Formalization of Abstract State Transition Systems for SAT
- Automata-based symbolic string analysis for vulnerability detection
- Flexible proof production in an industrial-strength SMT solver
- Solving String Theories Involving Regular Membership Predicates Using SAT
- Formalization of Basic Combinatorics on Words
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)
