{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,13]],"date-time":"2026-02-13T06:23:45Z","timestamp":1770963825718,"version":"3.50.1"},"reference-count":62,"publisher":"World Scientific Pub Co Pte Ltd","issue":"01","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int. J. Found. Comput. Sci."],"published-print":{"date-parts":[[2026,1]]},"abstract":"<jats:p>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 formalise the SMT-LIB theory of strings using Isabelle, an interactive theorem prover known for its ability to formalise 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.<\/jats:p>","DOI":"10.1142\/s0129054125410035","type":"journal-article","created":{"date-parts":[[2025,3,29]],"date-time":"2025-03-29T00:00:52Z","timestamp":1743206452000},"page":"47-71","source":"Crossref","is-referenced-by-count":0,"title":["Certainty in Formalising SMT-LIB for Strings in Isabelle"],"prefix":"10.1142","volume":"37","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6759-3304","authenticated-orcid":false,"given":"Kevin","family":"Lotz","sequence":"first","affiliation":[{"name":"Department of Computer Science, Kiel University, 24098 Kiel, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4650-1110","authenticated-orcid":false,"given":"Mitja","family":"Kulczynski","sequence":"additional","affiliation":[{"name":"Department of Computer Science, Kiel University, 24098 Kiel, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5422-2229","authenticated-orcid":false,"given":"Dirk","family":"Nowotka","sequence":"additional","affiliation":[{"name":"Department of Computer Science, Kiel University, 24098 Kiel, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9623-0748","authenticated-orcid":false,"given":"Danny B\u00f8gsted","family":"Poulsen","sequence":"additional","affiliation":[{"name":"Department of Computer Science, Aalborg University Copenhagen, A.C. Meyers V\u00e6nge 15, Copenhagen SV, Denmark"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9212-6150","authenticated-orcid":false,"given":"Anders","family":"Schlichtkrull","sequence":"additional","affiliation":[{"name":"Department of Computer Science, Aalborg University Copenhagen, A.C. Meyers V\u00e6nge 15, Copenhagen SV, Denmark"}]}],"member":"219","published-online":{"date-parts":[[2025,3,29]]},"reference":[{"key":"S0129054125410035BIB001","doi-asserted-by":"publisher","DOI":"10.23919\/FMCAD.2018.8602997"},{"key":"S0129054125410035BIB002","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_10"},{"key":"S0129054125410035BIB003","doi-asserted-by":"publisher","DOI":"10.23919\/FMCAD.2018.8602994"},{"key":"S0129054125410035BIB004","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"S0129054125410035BIB005","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-10769-6_3"},{"key":"S0129054125410035BIB006","unstructured":"C. Barrett, P. Fontaine and C. Tinelli, The SMT-LIB Standard: Version 2.6, tech. rep., Department of Computer Science, The University of Iowa (2017). Available at www.SMT-LIB.org."},{"key":"S0129054125410035BIB007","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8_11"},{"key":"S0129054125410035BIB008","doi-asserted-by":"publisher","DOI":"10.23919\/FMCAD.2017.8102241"},{"key":"S0129054125410035BIB009","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81688-9_14"},{"key":"S0129054125410035BIB010","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00768-2_27"},{"key":"S0129054125410035BIB011","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-9455-7"},{"key":"S0129054125410035BIB012","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40229-1_4"},{"key":"S0129054125410035BIB013","doi-asserted-by":"publisher","DOI":"10.24963\/ijcai.2017\/667"},{"key":"S0129054125410035BIB014","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14052-5_14"},{"key":"S0129054125410035BIB015","doi-asserted-by":"publisher","DOI":"10.1145\/321239.321249"},{"key":"S0129054125410035BIB016","doi-asserted-by":"publisher","DOI":"10.1145\/3290362"},{"key":"S0129054125410035BIB017","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-30806-3_8"},{"key":"S0129054125410035BIB018","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-00250-3_2"},{"key":"S0129054125410035BIB019","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"S0129054125410035BIB020","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-23021-4_2"},{"key":"S0129054125410035BIB021","doi-asserted-by":"publisher","DOI":"10.1145\/2685616"},{"key":"S0129054125410035BIB022","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-20652-9_10"},{"key":"S0129054125410035BIB023","unstructured":"M. Fleury, Formalization of logical calculi in Isabelle\/HOL, PhD thesis, Saarland University, Saarbr\u00fccken, Germany (2020)."},{"key":"S0129054125410035BIB024","first-page":"158","volume-title":"Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018","author":"Fleury M.","year":"2018"},{"key":"S0129054125410035BIB025","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.301.6"},{"key":"S0129054125410035BIB026","doi-asserted-by":"publisher","DOI":"10.29007\/96wb"},{"key":"S0129054125410035BIB027","doi-asserted-by":"publisher","DOI":"10.3390\/electronics7060081"},{"key":"S0129054125410035BIB028","unstructured":"F. Haftmann and L. Bulwahn, Code generation from Isabelle\/HOL theories (2024) https:\/\/www.cl.cam.ac.uk\/research\/hvg\/Isabelle\/dist\/Isabelle2024\/doc\/codegen.pdf."},{"key":"S0129054125410035BIB029","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12251-4_9"},{"key":"S0129054125410035BIB030","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-34175-6_2"},{"key":"S0129054125410035BIB031","series-title":"LIPIcs","first-page":"22:1","volume-title":"12th International Conference on Interactive Theorem Proving, ITP 2021","volume":"193","author":"Holub S.","year":"2021"},{"key":"S0129054125410035BIB032","series-title":"LIPIcs","first-page":"95:1","volume-title":"44th International Colloquium on Automata, Languages, and Programming, ICALP 2017","volume":"80","author":"Jez A.","year":"2017"},{"key":"S0129054125410035BIB033","doi-asserted-by":"publisher","DOI":"10.1145\/3497775.3503691"},{"key":"S0129054125410035BIB034","unstructured":"A. Krauss and T. Nipkow, Regular sets and expressions,\n                      Archive of Formal Proofs\n                      (May 2010), https:\/\/isa-afp.org\/entries\/Regular-Sets.html, Formal proof development."},{"key":"S0129054125410035BIB035","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-011-9223-4"},{"key":"S0129054125410035BIB036","unstructured":"M. Kulczynski, Light on string solving: Approaches to efficiently and correctly solving string constraints, PhD thesis, University of Kiel, Germany (2022)."},{"key":"S0129054125410035BIB037","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-78116-2_2"},{"key":"S0129054125410035BIB038","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-15077-7_8"},{"key":"S0129054125410035BIB039","doi-asserted-by":"publisher","DOI":"10.1145\/3387903.3389317"},{"key":"S0129054125410035BIB040","unstructured":"S. Lescuyer, Formalizing and implementing a reflexive tactic for automated deduction in Coq. (Formalisation et developpement d\u2019une tactique reflexive pour la demonstration automatique en Coq), PhD thesis, University of Paris-Sud, Orsay, France (2011)."},{"key":"S0129054125410035BIB041","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781107326019"},{"key":"S0129054125410035BIB042","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-40247-0_15"},{"key":"S0129054125410035BIB043","doi-asserted-by":"publisher","DOI":"10.1070\/SM1977v032n02ABEH002376"},{"key":"S0129054125410035BIB044","unstructured":"F. Mari\u0107, Formal verification of modern SAT solvers,\n                      Archive of Formal Proofs\n                      (July 2008) https:\/\/isa-afp.org\/entries\/SATSolverVerification.html, Formal proof development."},{"key":"S0129054125410035BIB045","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2010.09.014"},{"issue":"3","key":"S0129054125410035BIB046","volume":"7","author":"Maric F.","year":"2011","journal-title":"Log. Methods Comput. Sci."},{"key":"S0129054125410035BIB047","first-page":"132","volume":"8","author":"Matiyasevich Y. V.","year":"1968","journal-title":"Zapiski Nauchnykh Seminarov POMI"},{"key":"S0129054125410035BIB048","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-90870-6_21"},{"key":"S0129054125410035BIB049","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9"},{"key":"S0129054125410035BIB050","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27940-9_24"},{"key":"S0129054125410035BIB051","doi-asserted-by":"publisher","DOI":"10.1145\/2389836.2389853"},{"key":"S0129054125410035BIB052","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-13185-1_1"},{"key":"S0129054125410035BIB053","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2010.38"},{"key":"S0129054125410035BIB054","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.336.6"},{"key":"S0129054125410035BIB055","series-title":"Electronic Notes in Theoretical Computer Science","first-page":"3","volume-title":"Proceedings of the Fifth Logical and Semantic Frameworks, with Applications Workshop, LSFA 2010","volume":"269","author":"Shankar N.","year":"2010"},{"key":"S0129054125410035BIB056","doi-asserted-by":"publisher","DOI":"10.1145\/2522920.2522926"},{"key":"S0129054125410035BIB057","unstructured":"C. Tinelli, C. Barrett and P. Fontaine, SMT: Theory of strings http:\/\/smtlib.cs.uiowa. edu\/theories-UnicodeStrings.shtml, Accessed: 2022-03-03."},{"key":"S0129054125410035BIB058","unstructured":"M. Wenzel\n                      et al.\n                      , The Isabelle\/Isar reference manual (2004), https:\/\/www.cl.cam. ac.uk\/research\/hvg\/Isabelle\/dist\/Isabelle2024\/doc\/codegen.pdf."},{"key":"S0129054125410035BIB059","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_7"},{"key":"S0129054125410035BIB060","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-013-0189-1"},{"key":"S0129054125410035BIB061","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/jzaa062"},{"key":"S0129054125410035BIB062","doi-asserted-by":"publisher","DOI":"10.1145\/2491411.2491456"}],"container-title":["International Journal of Foundations of Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.worldscientific.com\/doi\/pdf\/10.1142\/S0129054125410035","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,13]],"date-time":"2026-02-13T05:37:15Z","timestamp":1770961035000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.worldscientific.com\/doi\/10.1142\/S0129054125410035"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,3,29]]},"references-count":62,"journal-issue":{"issue":"01","published-print":{"date-parts":[[2026,1]]}},"alternative-id":["10.1142\/S0129054125410035"],"URL":"https:\/\/doi.org\/10.1142\/s0129054125410035","relation":{},"ISSN":["0129-0541","1793-6373"],"issn-type":[{"value":"0129-0541","type":"print"},{"value":"1793-6373","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,3,29]]}}}