{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,22]],"date-time":"2025-10-22T10:50:08Z","timestamp":1761130208466,"version":"3.44.0"},"reference-count":65,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2025,7,21]],"date-time":"2025-07-21T00:00:00Z","timestamp":1753056000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,7,21]],"date-time":"2025-07-21T00:00:00Z","timestamp":1753056000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100001782","name":"University of Melbourne","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100001782","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2025,9]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Suffix arrays are a data structure with numerous real-world applications. They are extensively used in text retrieval and data compression applications, including query suggestion mechanisms in web search, and in bioinformatics tools for DNA sequencing and matching. This wide applicability means that algorithms for constructing suffix arrays are of great practical importance. The SA-IS algorithm is an efficient but conceptually complex suffix array construction technique, and implementing it requires a deep understanding of its underlying theory. As a critical step towards developing a provably correct and efficient implementation, we have developed the SA-IS algorithm in Isabelle\/HOL and formally verified that it is equivalent to a mathematical functional specification of suffix arrays, a task that required verifying a wide range of underlying properties of strings and suffixes. We also used Isabelle\u2019s code extraction facilities to extract an executable Haskell implementation of SA-IS, which albeit is inefficient due to using lists and natural numbers rather than arrays and machine words, demonstrates that our verified HOL implementation of SA-IS can be refined to an executable implementation in its current form.<\/jats:p>","DOI":"10.1007\/s10817-025-09735-8","type":"journal-article","created":{"date-parts":[[2025,7,21]],"date-time":"2025-07-21T06:40:31Z","timestamp":1753080031000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Formally Verified Suffix Array Construction"],"prefix":"10.1007","volume":"69","author":[{"given":"Louis","family":"Cheung","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alistair","family":"Moffat","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christine","family":"Rizkallah","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,7,21]]},"reference":[{"issue":"5","key":"9735_CR1","doi-asserted-by":"publisher","first-page":"935","DOI":"10.1137\/0222058","volume":"22","author":"U Manber","year":"1993","unstructured":"Manber, U., Myers, E.W.: Suffix arrays: A new method for on-line string searches. SIAM J. Comput. 22(5), 935\u2013948 (1993). https:\/\/doi.org\/10.1137\/0222058","journal-title":"SIAM J. Comput."},{"issue":"1","key":"9735_CR2","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1016\/S1570-8667(03)00065-0","volume":"2","author":"MI Abouelhoda","year":"2004","unstructured":"Abouelhoda, M.I., Kurtz, S., Ohlebusch, E.: Replacing suffix trees with enhanced suffix arrays. Journal of Discrete Algorithms 2(1), 53\u201386 (2004). https:\/\/doi.org\/10.1016\/S1570-8667(03)00065-0","journal-title":"Journal of Discrete Algorithms"},{"key":"9735_CR3","doi-asserted-by":"publisher","unstructured":"K\u00e4rkk\u00e4inen, J., Sanders, P.: Simple linear work suffix array construction. In: Proc. Automata, Languages and Programming. Lecture Notes in Computer Science, vol. 2719, pp. 943\u2013955. Springer, Eindhoven, The Netherlands (2003). https:\/\/doi.org\/10.1007\/3-540-45061-0_73","DOI":"10.1007\/3-540-45061-0_73"},{"issue":"2\u20134","key":"9735_CR4","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1016\/j.jda.2004.08.002","volume":"3","author":"P Ko","year":"2005","unstructured":"Ko, P., Aluru, S.: Space efficient linear time construction of suffix arrays. Journal of Discrete Algorithms 3(2\u20134), 143\u2013156 (2005). https:\/\/doi.org\/10.1016\/j.jda.2004.08.002","journal-title":"Journal of Discrete Algorithms"},{"key":"9735_CR5","doi-asserted-by":"publisher","unstructured":"Nong, G., Zhang, S., Chan, W.H.: Linear suffix array construction by almost pure induced-sorting. In: Proc. Data Compression Conference, pp. 193\u2013202. IEEE Computer Society, Snowbird, UT, USA (2009). https:\/\/doi.org\/10.1109\/DCC.2009.42","DOI":"10.1109\/DCC.2009.42"},{"issue":"10","key":"9735_CR6","doi-asserted-by":"publisher","first-page":"1471","DOI":"10.1109\/TC.2010.188","volume":"60","author":"G Nong","year":"2011","unstructured":"Nong, G., Zhang, S., Chan, W.H.: Two efficient algorithms for linear time suffix array construction. IEEE Trans. Comput. 60(10), 1471\u20131484 (2011). https:\/\/doi.org\/10.1109\/TC.2010.188","journal-title":"IEEE Trans. Comput."},{"key":"9735_CR7","volume-title":"A block-sorting lossless data compression algorithm","author":"M Burrows","year":"1994","unstructured":"Burrows, M., Wheeler, D.: A block-sorting lossless data compression algorithm. Technical report, Digital SRC Research Report (1994)"},{"key":"9735_CR8","unstructured":"Seward, J.: bzip2 Homepage. https:\/\/sourceware.org\/bzip2\/index.html. Accessed: 2023-09-12 (1996)"},{"issue":"4","key":"9735_CR9","doi-asserted-by":"publisher","first-page":"552","DOI":"10.1145\/1082036.1082039","volume":"52","author":"P Ferragina","year":"2005","unstructured":"Ferragina, P., Manzini, G.: Indexing compressed text. Journal of ACM 52(4), 552\u2013581 (2005). https:\/\/doi.org\/10.1145\/1082036.1082039","journal-title":"Indexing compressed text. Journal of ACM"},{"issue":"4","key":"9735_CR10","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1038\/nmeth.1923","volume":"9","author":"B Langmead","year":"2012","unstructured":"Langmead, B., Salzberg, S.L.: Fast gapped-read alignment with Bowtie 2. Nat. Methods 9(4), 357\u2013359 (2012). https:\/\/doi.org\/10.1038\/nmeth.1923","journal-title":"Nat. Methods"},{"issue":"3","key":"9735_CR11","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1186\/gb-2009-10-3-r25","volume":"10","author":"B Langmead","year":"2009","unstructured":"Langmead, B., Trapnell, C., Pop, M., Salzberg, S.L.: Ultrafast and memory-efficient alignment of short DNA sequences to the human genome. Genome Biol. 10(3), 25 (2009). https:\/\/doi.org\/10.1186\/gb-2009-10-3-r25","journal-title":"Genome Biol."},{"issue":"14","key":"9735_CR12","doi-asserted-by":"publisher","first-page":"1754","DOI":"10.1093\/bioinformatics\/btp324","volume":"25","author":"H Li","year":"2009","unstructured":"Li, H., Durbin, R.: Fast and accurate short read alignment with Burrows-Wheeler transform. Bioinformatics 25(14), 1754\u20131760 (2009). https:\/\/doi.org\/10.1093\/bioinformatics\/btp324","journal-title":"Bioinformatics"},{"issue":"15","key":"9735_CR13","doi-asserted-by":"publisher","first-page":"1966","DOI":"10.1093\/bioinformatics\/btp336","volume":"25","author":"R Li","year":"2009","unstructured":"Li, R., Yu, C., Li, Y., Lam, T.W., Yiu, S., Kristiansen, K., Wang, J.: SOAP2: An improved ultrafast tool for short read alignment. Bioinformatics 25(15), 1966\u20131967 (2009). https:\/\/doi.org\/10.1093\/bioinformatics\/btp336","journal-title":"Bioinformatics"},{"key":"9735_CR14","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science, vol. 2283. Springer, Berlin, Heidelberg (2002)","DOI":"10.1007\/3-540-45949-9"},{"key":"9735_CR15","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511546853","volume-title":"Algorithms on Strings","author":"M Crochemore","year":"2007","unstructured":"Crochemore, M., Hancart, C., Lecroq, T.: Algorithms on Strings. Cambridge University Press, Cambridge (2007)"},{"key":"9735_CR16","doi-asserted-by":"publisher","unstructured":"Nipkow, T., Klein, G.: Concrete Semantics - With Isabelle\/HOL. Springer, Berlin, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-319-10542-0","DOI":"10.1007\/978-3-319-10542-0"},{"issue":"2","key":"9735_CR17","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1145\/1242471.1242472","volume":"39","author":"SJ Puglisi","year":"2007","unstructured":"Puglisi, S.J., Smyth, W.F., Turpin, A.: A taxonomy of suffix array construction algorithms. ACM Computing Survey 39(2), 4 (2007). https:\/\/doi.org\/10.1145\/1242471.1242472","journal-title":"ACM Computing Survey"},{"key":"9735_CR18","doi-asserted-by":"publisher","unstructured":"Itoh, H., Tanaka, H.: An efficient method for in memory construction of suffix arrays. In: Proc. String Processing and Information Retrieval, pp. 81\u201388. IEEE Computer Society, Cancun, Mexico (1999). https:\/\/doi.org\/10.1109\/SPIRE.1999.796581","DOI":"10.1109\/SPIRE.1999.796581"},{"key":"9735_CR19","unstructured":"Fischer, J., Kurpicz, F.: Dismantling DivSufSort. CoRR abs\/1710.01896 (2017) arXiv:arXiv:1710.01896"},{"key":"9735_CR20","doi-asserted-by":"crossref","unstructured":"Gordon, M., Milner, R., Wadsworth, C.P.: Edinburgh LCF. Lecture Notes in Computer Science, vol. 78. Springer, Berlin, Heidelberg (1979)","DOI":"10.1007\/3-540-09724-4"},{"key":"9735_CR21","volume-title":"Definition of Standard ML","author":"R Milner","year":"1990","unstructured":"Milner, R., Tofte, M., Harper, R.: Definition of Standard ML. MIT Press, Cambridge, Massachusetts, USA (1990)"},{"key":"9735_CR22","unstructured":"Minsky, Y., Madhavapeddy, A., Hickey, J.: Real World OCaml - Functional Programming for the Masses. O\u2019Reilly, Sebastopol, California, USA (2013)"},{"issue":"1","key":"9735_CR23","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1017\/S0956796803000315","volume":"13","author":"S Jones","year":"2003","unstructured":"Jones, S.: Haskell 98: Introduction. J. Funct. Program. 13(1), 6 (2003). https:\/\/doi.org\/10.1017\/S0956796803000315","journal-title":"J. Funct. Program."},{"key":"9735_CR24","unstructured":"Odersky, M., Altherr, P., Cremet, B., Dragos, I., Dubochet, G., Emir, B., McDirmid, S., Micheloud, S., Mihaylov, N., Schinz, M., Stenman, E., Spoon, L., Zenger, M.: An overview of the Scala programming language. Technical report, EPFL, Lausanne, Switzerland (2004). https:\/\/infoscience.epfl.ch\/handle\/20.500.14299\/214698"},{"key":"9735_CR25","doi-asserted-by":"publisher","unstructured":"Haftmann, F., Nipkow, T.: Code generation via higher-order rewrite systems. In: Proc. Functional and Logic Programming. Lecture Notes in Computer Science, vol. 6009, pp. 103\u2013117. Springer, Sendai, Japan (2010). https:\/\/doi.org\/10.1007\/978-3-642-12251-4_9","DOI":"10.1007\/978-3-642-12251-4_9"},{"key":"9735_CR26","doi-asserted-by":"crossref","unstructured":"Cheung, L., Rizkallah, C.: Formally verified suffix array construction. Archive of Formal Proofs (2024). https:\/\/isa-afp.org\/entries\/SuffixArray.html, Formal proof development","DOI":"10.1007\/s10817-025-09735-8"},{"key":"9735_CR27","doi-asserted-by":"publisher","unstructured":"Cheung, L., O\u2019Connor, L., Rizkallah, C.: Overcoming restraint: Composing verification of foreign functions with Cogent. In: Proc. Certified Programs and Proofs, pp. 13\u201326. ACM, Philadelphia, PA, USA (2022). https:\/\/doi.org\/10.1145\/3497775.3503686","DOI":"10.1145\/3497775.3503686"},{"key":"9735_CR28","doi-asserted-by":"publisher","unstructured":"Matichuk, D., Murray, T., Andronick, J., Jeffery, R., Klein, G., Staples, M.: Empirical study towards a leading indicator for cost of formal software verification. In: 2015 IEEE\/ACM 37th IEEE International Conference on Software Engineering. ICSE, vol. 1, pp. 722\u2013732 (2015). https:\/\/doi.org\/10.1109\/ICSE.2015.85","DOI":"10.1109\/ICSE.2015.85"},{"issue":"2\u20133","key":"9735_CR29","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1561\/2500000045","volume":"5","author":"T Ringer","year":"2019","unstructured":"Ringer, T., Palmskog, K., Sergey, I., Gligoric, M., Tatlock, Z.: QED at large: A survey of engineering of formally verified software. Foundations and Trends in Programming Languages 5(2\u20133), 102\u2013281 (2019). https:\/\/doi.org\/10.1561\/2500000045","journal-title":"Foundations and Trends in Programming Languages"},{"issue":"4","key":"9735_CR30","doi-asserted-by":"publisher","first-page":"481","DOI":"10.1007\/S10817-017-9437-1","volume":"62","author":"P Lammich","year":"2019","unstructured":"Lammich, P.: Refinement to imperative HOL. Journal of Automatic Reasoning 62(4), 481\u2013503 (2019). https:\/\/doi.org\/10.1007\/S10817-017-9437-1","journal-title":"Journal of Automatic Reasoning"},{"key":"9735_CR31","doi-asserted-by":"publisher","unstructured":"Zhan, B., Haslbeck, M.P.L.: Verifying asymptotic time complexity of imperative programs in Isabelle. In: Proc. International Joint Conference on Automated Reasoning. Lecture Notes in Computer Science, vol. 10900, pp. 532\u2013548. Springer, Oxford, UK (2018). https:\/\/doi.org\/10.1007\/978-3-319-94205-6_35","DOI":"10.1007\/978-3-319-94205-6_35"},{"issue":"3","key":"9735_CR32","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1145\/2493175.2493180","volume":"31","author":"G Nong","year":"2013","unstructured":"Nong, G.: Practical linear-time O(1)-workspace suffix sorting for constant alphabets. ACM Transactions on Information Systems 31(3), 15 (2013). https:\/\/doi.org\/10.1145\/2493175.2493180","journal-title":"ACM Transactions on Information Systems"},{"key":"9735_CR33","doi-asserted-by":"publisher","DOI":"10.1016\/J.IC.2021.104818","volume":"285","author":"Z Li","year":"2022","unstructured":"Li, Z., Li, J., Huo, H.: Optimal in-place suffix sorting. Inf. Comput. 285, 104818 (2022). https:\/\/doi.org\/10.1016\/J.IC.2021.104818","journal-title":"Inf. Comput."},{"key":"9735_CR34","unstructured":"Goto, K.: Optimal time and space construction of suffix arrays and LCP arrays for integer alphabets. In: Holub, J., Zd\u00e1rek, J. (eds.) Proc. Prague Stringtology, pp. 111\u2013125. Czech Technical University in Prague, Faculty of Information Technology, Department of Theoretical Computer Science, ??? (2019). arXiv:arXiv:1703.01009v5"},{"key":"9735_CR35","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3549992","volume":"27","author":"D Nunes","year":"2022","unstructured":"Nunes, D., Louza, F.A., Gog, S., Ayala-Rinc\u00f3n, M., Navarro, G.: Grammar compression by induced suffix sorting. Journal of Experimental Algorithms 27, 1\u2013111133 (2022). https:\/\/doi.org\/10.1145\/3549992","journal-title":"Journal of Experimental Algorithms"},{"key":"9735_CR36","doi-asserted-by":"publisher","unstructured":"Kasai, T., Lee, G., Arimura, H., Arikawa, S., Park, K.: Linear-time longest-common-prefix computation in suffix arrays and its applications. In: Proc. Combinatorial Pattern Matching. Lecture Notes in Computer Science, vol. 2089, pp. 181\u2013192. Springer, ??? (2001). https:\/\/doi.org\/10.1007\/3-540-48194-X_17","DOI":"10.1007\/3-540-48194-X_17"},{"key":"9735_CR37","doi-asserted-by":"publisher","unstructured":"Cheung, L., Moffat, A., Rizkallah, C.: Formalized Burrows-Wheeler transform. In: Proc. Certified Programs and Proofs, pp. 13\u201326. ACM, ??? (2025). https:\/\/doi.org\/10.1145\/3703595.3705883","DOI":"10.1145\/3703595.3705883"},{"key":"9735_CR38","doi-asserted-by":"crossref","unstructured":"Cheung, L., Rizkallah, C.: Formalised Burrows-Wheeler transform. Archive of Formal Proofs (2025). https:\/\/isa-afp.org\/entries\/BurrowsWheeler.html, Formal proof development","DOI":"10.1145\/3703595.3705883"},{"issue":"3","key":"9735_CR39","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1016\/J.TCS.2007.07.017","volume":"387","author":"NJ Larsson","year":"2007","unstructured":"Larsson, N.J., Sadakane, K.: Faster suffix sorting. Theory of Computer Science 387(3), 258\u2013272 (2007). https:\/\/doi.org\/10.1016\/J.TCS.2007.07.017","journal-title":"Theory of Computer Science"},{"key":"9735_CR40","doi-asserted-by":"publisher","unstructured":"Karp, R.M., Miller, R.E., Rosenberg, A.L.: Rapid identification of repeated patterns in strings, trees and arrays. In: Proc. Symposium on Theory of Computing, pp. 125\u2013136. ACM, Denver, Colorado, USA (1972). https:\/\/doi.org\/10.1145\/800152.804905","DOI":"10.1145\/800152.804905"},{"key":"9735_CR41","doi-asserted-by":"publisher","unstructured":"Farach, M.: Optimal suffix tree construction with large alphabets. In: Proc. Symposium on Foundations of Computer Science, pp. 137\u2013143. IEEE Computer Society, Miami Beach, Florida, USA (1997). https:\/\/doi.org\/10.1109\/SFCS.1997.646102","DOI":"10.1109\/SFCS.1997.646102"},{"key":"9735_CR42","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1227161.1278374","volume":"12","author":"MA Maniscalco","year":"2007","unstructured":"Maniscalco, M.A., Puglisi, S.J.: An efficient, versatile approach to suffix sorting. Journal of Experimental Algorithms 12, 1\u2013211223 (2007). https:\/\/doi.org\/10.1145\/1227161.1278374","journal-title":"Journal of Experimental Algorithms"},{"key":"9735_CR43","doi-asserted-by":"publisher","unstructured":"Nipkow, T., Eberl, M., Haslbeck, M.P.L.: Verified textbook algorithms: A biased survey. In: Proc. Automated Technology for Verification and Analysis. Lecture Notes in Computer Science, vol. 12302, pp. 25\u201353. Springer, Hanoi, Vietnam (2020). https:\/\/doi.org\/10.1007\/978-3-030-59152-6_2","DOI":"10.1007\/978-3-030-59152-6_2"},{"key":"9735_CR44","unstructured":"Appel, A.W.: Verified Functional Algorithms. Software Foundations, vol. 3. Electronic textbook, Online (2024). Version 1.5.5, http:\/\/softwarefoundations.cis.upenn.edu"},{"issue":"6","key":"9735_CR45","doi-asserted-by":"publisher","first-page":"729","DOI":"10.1007\/s10009-013-0293-y","volume":"17","author":"D Bruns","year":"2015","unstructured":"Bruns, D., Mostowski, W., Ulbrich, M.: Implementation-level verification of algorithms with KeY. Int. J. Softw. Tools Technol. Transfer 17(6), 729\u2013744 (2015). https:\/\/doi.org\/10.1007\/s10009-013-0293-y","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"issue":"6","key":"9735_CR46","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1007\/s10009-014-0308-3","volume":"17","author":"G Ernst","year":"2015","unstructured":"Ernst, G., Pf\u00e4hler, J., Schellhorn, G., Haneberg, D., Reif, W.: KIV: Overview and VerifyThis competition. Int. J. Softw. Tools Technol. Transfer 17(6), 677\u2013694 (2015). https:\/\/doi.org\/10.1007\/s10009-014-0308-3","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"issue":"6","key":"9735_CR47","doi-asserted-by":"publisher","first-page":"709","DOI":"10.1007\/s10009-014-0314-5","volume":"17","author":"F Bobot","year":"2015","unstructured":"Bobot, F., Filli\u00e2tre, J., March\u00e9, C., Paskevich, A.: Let\u2019s verify this with Why3. Int. J. Softw. Tools Technol. Transfer 17(6), 709\u2013727 (2015). https:\/\/doi.org\/10.1007\/s10009-014-0314-5","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"issue":"6","key":"9735_CR48","doi-asserted-by":"publisher","first-page":"647","DOI":"10.1007\/s10009-015-0396-8","volume":"17","author":"M Huisman","year":"2015","unstructured":"Huisman, M., Klebanov, V., Monahan, R.: VerifyThis 2012: A program verification competition. Int. J. Softw. Tools Technol. Transfer 17(6), 647\u2013657 (2015). https:\/\/doi.org\/10.1007\/s10009-015-0396-8","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"9735_CR49","doi-asserted-by":"publisher","unstructured":"Dramnesc, I., Jebelean, T., Stratulat, S.: Certification of sorting algorithms using Theorema and Coq. In: Proc. International Symposium on Symbolic Computation in Softward Science. Lecture Notes in Computer Science, vol. 14991, pp. 38\u201356. Springer, Tokyo, Japan (2024). https:\/\/doi.org\/10.1007\/978-3-031-69042-6_3","DOI":"10.1007\/978-3-031-69042-6_3"},{"key":"9735_CR50","unstructured":"Griebel, S.: Binary heaps for IMP2. Archive of Formal Proofs (2019). https:\/\/isa-afp.org\/entries\/IMP2_Binary_Heap.html, Formal proof development"},{"key":"9735_CR51","unstructured":"Sternagel, C.: Imperative insertion sort. Archive of Formal Proofs (2014). https:\/\/isa-afp.org\/entries\/Imperative_Insertion_Sort.html, Formal proof development"},{"key":"9735_CR52","doi-asserted-by":"publisher","unstructured":"Beckert, B., Sanders, P., Ulbrich, M., Wiesler, J., Witt, S.: Formally verifying an efficient sorter. In: Proc. Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 14570, pp. 268\u2013287. Springer, Luxembourg City, Luxembourg (2024). https:\/\/doi.org\/10.1007\/978-3-031-57246-3_15","DOI":"10.1007\/978-3-031-57246-3_15"},{"key":"9735_CR53","doi-asserted-by":"publisher","unstructured":"Lammich, P.: Efficient verified implementation of Introsort and Pdqsort. In: Proc. International Joint Conference on Automated Reasoning. Lecture Notes in Computer Science, vol. 12167, pp. 307\u2013323. Springer, Berlin, Heidelberg (2020). https:\/\/doi.org\/10.1007\/978-3-030-51054-1_18","DOI":"10.1007\/978-3-030-51054-1_18"},{"key":"9735_CR54","doi-asserted-by":"publisher","unstructured":"Knuth, D.E., Jr., J.H.M., Pratt, V.R.: Fast pattern matching in strings. SIAM Journal on Computing 6(2), 323\u2013350 (1977). https:\/\/doi.org\/10.1137\/0206024","DOI":"10.1137\/0206024"},{"issue":"10","key":"9735_CR55","doi-asserted-by":"publisher","first-page":"762","DOI":"10.1145\/359842.359859","volume":"20","author":"RS Boyer","year":"1977","unstructured":"Boyer, R.S., Moore, J.S.: A fast string searching algorithm. Commun. ACM 20(10), 762\u2013772 (1977). https:\/\/doi.org\/10.1145\/359842.359859","journal-title":"Commun. ACM"},{"key":"9735_CR56","unstructured":"Hellauer, F., Lammich, P.: The string search algorithm by Knuth, Morris and Pratt. Archive of Formal Proofs (2017). https:\/\/isa-afp.org\/entries\/Knuth_nMorris_Pratt.html, Formal proof development"},{"key":"9735_CR57","unstructured":"Paulson, L.C.: Knuth\u2013Morris\u2013Pratt string search. Archive of Formal Proofs (2023). https:\/\/isa-afp.org\/entries\/KnuthMorrisPratt.html, Formal proof development"},{"key":"9735_CR58","doi-asserted-by":"publisher","unstructured":"Filli\u00e2tre, J.: Proof of imperative programs in type theory. In: Types for Proofs and Programs. Lecture Notes in Computer Science, vol. 1657, pp. 78\u201392. Springer, Kloster Irsee, Germany (1998). https:\/\/doi.org\/10.1007\/3-540-48167-2_6","DOI":"10.1007\/3-540-48167-2_6"},{"key":"9735_CR59","unstructured":"Boyer, R.S., Moore, J.S.: A Computational Logic Handbook. Perspectives in Computing, vol. 23. Academic Press, Cambridge, Massachusetts, USA (1979)"},{"key":"9735_CR60","doi-asserted-by":"publisher","unstructured":"Moore, J.S., Martinez, M.: A mechanically checked proof of the correctness of the Boyer-Moore fast string searching algorithm. In: Engineering Methods and Tools for Software Safety and Security. NATO Science for Peace and Security Series - D: Information and Communication Security, vol. 22, pp. 267\u2013284. IOS Press, Amsterdam, The Netherlands (2009). https:\/\/doi.org\/10.3233\/978-1-58603-976-9-267","DOI":"10.3233\/978-1-58603-976-9-267"},{"key":"9735_CR61","doi-asserted-by":"publisher","unstructured":"Lammich, P.: Generating verified LLVM from Isabelle\/HOL. In: Proc. Interactive Theorem Proving. LIPIcs, vol. 141, pp. 22\u201312219. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, Portland, Oregon, USA (2019). https:\/\/doi.org\/10.4230\/LIPICS.ITP.2019.22","DOI":"10.4230\/LIPICS.ITP.2019.22"},{"key":"9735_CR62","doi-asserted-by":"publisher","unstructured":"Noschinski, L., Rizkallah, C., Mehlhorn, K.: Verification of certifying computations through AutoCorres and Simpl. In: Proc. NASA Formal Methods Symposium, 46\u201361 (2014). https:\/\/doi.org\/10.1007\/978-3-319-06200-6_4","DOI":"10.1007\/978-3-319-06200-6_4"},{"key":"9735_CR63","doi-asserted-by":"publisher","unstructured":"Greenaway, D., Andronick, J., Klein, G.: Bridging the gap: Automatic verified abstraction of C. In: Proc. Interactive Theorem Proving. Lecture Notes in Computer Science, vol. 7406, pp. 99\u2013115. Springer, Princeton, New Jersey, USA (2012).https:\/\/doi.org\/10.1007\/978-3-642-32347-8_8","DOI":"10.1007\/978-3-642-32347-8_8"},{"key":"9735_CR64","doi-asserted-by":"publisher","unstructured":"O\u2019Connor, L., Chen, Z., Rizkallah, C., Amani, S., Lim, J., Murray, T.C., Nagashima, Y., Sewell, T., Klein, G.: Refinement through restraint: Bringing down the cost of verification. In: Proc. International Conference on Functional Programming, pp. 89\u2013102. ACM, Nara, Japan (2016). https:\/\/doi.org\/10.1145\/2951913.2951940","DOI":"10.1145\/2951913.2951940"},{"key":"9735_CR65","doi-asserted-by":"publisher","unstructured":"Rizkallah, C., Lim, J., Nagashima, Y., Sewell, T., Chen, Z., O\u2019Connor, L., Murray, T.C., Keller, G., Klein, G.: A framework for the automatic formal verification of refinement from Cogent to C. In: Proc. Interactive Theorem Proving. Lecture Notes in Computer Science, vol. 9807, pp. 323\u2013340. Springer, Nancy, France (2016). https:\/\/doi.org\/10.1007\/978-3-319-43144-4_20","DOI":"10.1007\/978-3-319-43144-4_20"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-025-09735-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-025-09735-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-025-09735-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,23]],"date-time":"2025-09-23T22:02:23Z","timestamp":1758664943000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-025-09735-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,7,21]]},"references-count":65,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2025,9]]}},"alternative-id":["9735"],"URL":"https:\/\/doi.org\/10.1007\/s10817-025-09735-8","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2025,7,21]]},"assertion":[{"value":"9 December 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"3 July 2025","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"21 July 2025","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Competing Interests"}},{"value":"No ethics approvals were required for this article.","order":3,"name":"Ethics","group":{"name":"EthicsHeading","label":"Ethics Approval"}}],"article-number":"21"}}