Verified Verifying: SMT-LIB for Strings in Isabelle

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

Publikation: Bidrag til bog/antologi/rapport/konference proceedingKonferenceartikel i proceedingForskningpeer 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.

TitelImplementation and Application of Automata - 27th International Conference, CIAA 2023, Proceedings
RedaktørerBenedek Nagy
Antal sider12
Publikationsdato10 aug. 2023
ISBN (Trykt)9783031402463
StatusUdgivet - 10 aug. 2023
BegivenhedInternational Conference on Implementation and Application of Automata -
Varighed: 19 sep. 202322 sep. 2023
Konferencens nummer: 27


KonferenceInternational Conference on Implementation and Application of Automata
NavnLecture Notes in Computer Science


Dyk ned i forskningsemnerne om 'Verified Verifying: SMT-LIB for Strings in Isabelle'. Sammen danner de et unikt fingeraftryk.