Verified verifying: SMT-LIB for strings in Isabelle
From MaRDI portal
Publication:6199876
DOI10.1007/978-3-031-40247-0_15OpenAlexW4385701414MaRDI QIDQ6199876
Anders Schlichtkrull, Mitja Kulczynski, Danny Bøgsted Poulsen, Kevin Lotz, Dirk Nowotka
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
- Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL
- An SMT solver for regular expressions and linear arithmetic over string length
- Isabelle/HOL. A proof assistant for higher-order logic
- A verified SAT solver framework with learn, forget, restart, and incrementality
- Flexible proof production in an industrial-strength SMT solver
- Automata-based symbolic string analysis for vulnerability detection
- On solving word equations using SAT
- Proof Pearl: regular expression equivalence and relation algebra
- A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality
- versat: A Verified Modern SAT Solver
- Satisfiability Modulo Theories
- Formalization of Abstract State Transition Systems for SAT
- The Isabelle Framework
- Path Feasibility Analysis for String-Manipulating Programs
- The Mechanical Verification of a DPLL-Based Satisfiability Solver
- Derivatives of Regular Expressions
- Fast LCF-Style Proof Reconstruction for Z3
- Formalization of Basic Combinatorics on Words
This page was built for publication: Verified verifying: SMT-LIB for strings in Isabelle
