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

Abstract

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.

OriginalsprogEngelsk
TitelImplementation and Application of Automata - 27th International Conference, CIAA 2023, Proceedings
RedaktørerBenedek Nagy
Antal sider12
Publikationsdato10 aug. 2023
Sider206-217
ISBN (Trykt)9783031402463
DOI
StatusUdgivet - 10 aug. 2023
BegivenhedInternational Conference on Implementation and Application of Automata -
Varighed: 19 sep. 202322 sep. 2023
Konferencens nummer: 27
https://ciaa.emu.edu.tr/en

Konference

KonferenceInternational Conference on Implementation and Application of Automata
Nummer27
Periode19/09/202322/09/2023
Internetadresse
NavnLecture Notes in Computer Science
ISSN0302-9743

Fingeraftryk

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

Citationsformater