Verified Verifying: SMT-LIB for Strings in Isabelle

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

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review


The prevalence of string solvers in formal program analysis has led to an increasing demand for more effective and dependable solving techniques. However, solving the satisfiability problem of string constraints, which is a generally undecidable problem, requires a deep understanding of the structure of the constraints. To address this challenge, the community has relied on SMT solvers to tackle the quantifier-free first-order logic fragment of string constraints, usually stated in SMT-LIB format. In 2020, the SMT-LIB Initiative issued the first official standard for string constraints. However, SMT-LIB states the semantics in a semi-formal manner, lacking a level of formality that is desirable for validating SMT solvers. In response, we formalize the SMT-LIB theory of strings using Isabelle, an interactive theorem prover known for its ability to formalize and verify mathematical and logical theorems. We demonstrate the usefulness of having a formally defined theory by deriving, to the best of our knowledge, the first automated verified model verification method for SMT-LIB string constraints and highlight potential future applications.

Original languageEnglish
Title of host publicationImplementation and Application of Automata - 27th International Conference, CIAA 2023, Proceedings
EditorsBenedek Nagy
Number of pages12
Publication date10 Aug 2023
ISBN (Print)9783031402463
Publication statusPublished - 10 Aug 2023
EventInternational Conference on Implementation and Application of Automata -
Duration: 19 Sept 202322 Sept 2023
Conference number: 27


ConferenceInternational Conference on Implementation and Application of Automata
Internet address
SeriesLecture Notes in Computer Science


Dive into the research topics of 'Verified Verifying: SMT-LIB for Strings in Isabelle'. Together they form a unique fingerprint.

Cite this