TY - GEN
T1 - Verified Verifying
T2 - 27th International Conference, CIAA 2023
AU - Lotz, Kevin
AU - Kulczynski, Mitja
AU - Nowotka, Dirk
AU - Poulsen, Danny Bøgsted
AU - Schlichtkrull, Anders
PY - 2023/8/10
Y1 - 2023/8/10
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85172080425&partnerID=8YFLogxK
U2 - 10.1007/978-3-031-40247-0_15
DO - 10.1007/978-3-031-40247-0_15
M3 - Article in proceeding
SN - 9783031402463
T3 - Lecture Notes in Computer Science
SP - 206
EP - 217
BT - Implementation and Application of Automata
A2 - Nagy, Benedek
PB - Springer Nature Switzerland AG
Y2 - 19 September 2023 through 22 September 2023
ER -