{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T09:05:52Z","timestamp":1784797552602,"version":"3.55.0"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032325259","type":"print"},{"value":"9783032325266","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,7,24]],"date-time":"2026-07-24T00:00:00Z","timestamp":1784851200000},"content-version":"vor","delay-in-days":204,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    We present\n                    <jats:sc>ZipLex<\/jats:sc>\n                    , a verified framework for invertible linear-time lexical analysis following the longest match (maximal munch) semantics. Unlike past verified lexers that focus only on satisfying the semantics of regular expressions and the longest match property,\n                    <jats:sc>ZipLex<\/jats:sc>\n                    also guarantees that lexing and printing are mutual inverses. Thanks to verified memoization, it also ensures that the lexical analysis of a string is linear in the size of the string. Our design and implementation rely on two sets of ideas: (1) a new abstraction of token sequences that captures the separability of tokens in a sequence while supporting their efficient manipulation, and (2) a combination of verified data structures and optimizations, including Huet\u2019s zippers and memoization with a standalone verified imperative hash table. Our hash table offers competitive performance as shown by our evaluation. We implemented and verified\n                    <jats:sc>ZipLex<\/jats:sc>\n                    using the Stainless deductive verifier for Scala. Our evaluation demonstrates that\n                    <jats:sc>ZipLex<\/jats:sc>\n                    supports realistic applications such as JSON processing and lexers of programming languages, and behaves linearly even in cases that make flex-style approaches quadratic.\n                    <jats:sc>ZipLex<\/jats:sc>\n                    is two orders of magnitude faster than Verbatim, showing that verified invertibility and linear-time algorithms can be developed without prohibitive cost. Compared to Coqlex,\n                    <jats:sc>ZipLex<\/jats:sc>\n                    also offers linear (instead of quadratic) time lexing, and is the first lexer that comes with invertibility proofs for printing token sequences.\n                  <\/jats:p>","DOI":"10.1007\/978-3-032-32526-6_7","type":"book-chapter","created":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T08:44:29Z","timestamp":1784796269000},"page":"141-164","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Formally Verified Linear-Time Invertible Lexing"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0000-9751-9252","authenticated-orcid":false,"given":"Samuel","family":"Chassot","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7044-9522","authenticated-orcid":false,"given":"Viktor","family":"Kun\u010dak","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,7,24]]},"reference":[{"key":"7_CR1","unstructured":"epfl-lara\/bolts. https:\/\/github.com\/epfl-lara\/bolts (Apr 2026), https:\/\/github.com\/epfl-lara\/bolts, original-date: 2017-10-12T10:48:10Z"},{"key":"7_CR2","doi-asserted-by":"publisher","unstructured":"Brachth\u00e4user, J.I., Rendel, T., Ostermann, K.: Parsing with first-class derivatives. In: Visser, E., Smaragdakis, Y. (eds.) Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2016, part of SPLASH 2016, Amsterdam, The Netherlands, October 30 - November 4, 2016, pp. 588\u2013606. ACM (2016). https:\/\/doi.org\/10.1145\/2983990.2984026","DOI":"10.1145\/2983990.2984026"},{"key":"7_CR3","doi-asserted-by":"publisher","unstructured":"Brzozowski, J.A.: Derivatives of regular expressions. J. ACM 11(4), 481\u2013494 (1964). https:\/\/doi.org\/10.1145\/321239.321249","DOI":"10.1145\/321239.321249"},{"key":"7_CR4","doi-asserted-by":"publisher","unstructured":"Bucev, M., Chassot, S., Felix, S., Schramka, F., Kuncak, V.: Formally verifiable generated ASN.1\/ACN encoders and decoders: a case study. In: Krishna, S., Sankaranarayanan, S., Trivedi, A. (eds.) Verification, Model Checking, and Abstract Interpretation - 26th International Conference, VMCAI 2025, Denver, CO, USA, January 20-21, 2025, Proceedings, Part II, pp. 185\u2013207. LNCS. Springer (2025). https:\/\/doi.org\/10.1007\/978-3-031-82703-7_9","DOI":"10.1007\/978-3-031-82703-7_9"},{"key":"7_CR5","doi-asserted-by":"publisher","unstructured":"Bucev, M., Kun\u010dak, V.: Formally verified quite OK image format. In: Griggio, A., Rungta, N. (eds.) 22nd Formal Methods in Computer-Aided Design, FMCAD 2022, Trento, Italy, October 17-21, 2022, pp. 343\u2013348. IEEE (2022). https:\/\/doi.org\/10.34727\/2022\/ISBN.978-3-85448-053-2_41","DOI":"10.34727\/2022\/ISBN.978-3-85448-053-2_41"},{"key":"7_CR6","unstructured":"Cattell, R.G.G.: Formalization and automatic derivation of code generators. Tech. rep., Carnegie-Mellon University, Dept.\u00a0of Computer Science (1978)"},{"key":"7_CR7","doi-asserted-by":"publisher","unstructured":"Chassot, S., Kun\u010dak, V.: Verifying a realistic mutable hash table. In: Benzm\u00fcller, C., Heule, M.J., Schmidt, R.A. (eds.) Automated Reasoning, pp. 304\u2013314. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-63498-7_18","DOI":"10.1007\/978-3-031-63498-7_18"},{"key":"7_CR8","doi-asserted-by":"publisher","unstructured":"Chassot, S., Kun\u010dak, V.: Formally verified linear-time invertible lexing (2026). https:\/\/doi.org\/10.48550\/arXiv.2510.18479, https:\/\/arxiv.org\/abs\/2510.18479","DOI":"10.48550\/arXiv.2510.18479"},{"key":"7_CR9","doi-asserted-by":"publisher","unstructured":"Chassot, S., Kun\u010dak, V.: Formally Verified Linear-Time Invertible Lexing (Artifact). https:\/\/zenodo.org\/records\/19830775, May 2026. https:\/\/doi.org\/10.5281\/zenodo.19830775","DOI":"10.5281\/zenodo.19830775"},{"key":"7_CR10","doi-asserted-by":"publisher","unstructured":"Chattopadhyay, A., Li, A.W., Mamouras, K.: Verified and efficient matching of regular expressions with lookaround. In: Proceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 198\u2013213. CPP \u201925. Association for Computing Machinery, New York, January 2025. https:\/\/doi.org\/10.1145\/3703595.3705884","DOI":"10.1145\/3703595.3705884"},{"key":"7_CR11","doi-asserted-by":"publisher","unstructured":"Darragh, P., Adams, M.D.: Parsing with zippers (functional pearl). Proc. ACM Program. Lang. 4(ICFP), 108:1\u2013108:28 (2020). https:\/\/doi.org\/10.1145\/3408990","DOI":"10.1145\/3408990"},{"key":"7_CR12","doi-asserted-by":"publisher","unstructured":"Edelmann, R.: Efficient Parsing with Derivatives and Zippers. Ph.D. thesis, EPFL (2021). https:\/\/doi.org\/10.5075\/epfl-thesis-7357, https:\/\/infoscience.epfl.ch\/handle\/20.500.14299\/179767","DOI":"10.5075\/epfl-thesis-7357"},{"key":"7_CR13","doi-asserted-by":"publisher","unstructured":"Edelmann, R., Hamza, J., Kuncak, V.: Zippy LL(1) parsing with derivatives. In: Donaldson, A.F., Torlak, E. (eds.) Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2020, London, UK, June 15-20, 2020, pp. 1036\u20131051. ACM (2020). https:\/\/doi.org\/10.1145\/3385412.3385992","DOI":"10.1145\/3385412.3385992"},{"key":"7_CR14","doi-asserted-by":"publisher","unstructured":"Egolf, D., Lasser, S., Fisher, K.: Verbatim: a verified lexer generator. In: 2021 IEEE Security and Privacy Workshops (SPW), pp. 92\u2013100. IEEE, San Francisco, May 2021. https:\/\/doi.org\/10.1109\/SPW53761.2021.00022","DOI":"10.1109\/SPW53761.2021.00022"},{"key":"7_CR15","doi-asserted-by":"publisher","unstructured":"Egolf, D., Lasser, S., Fisher, K.: Verbatim++: verified, optimized, and semantically rich lexing with derivatives. In: Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 27\u201339. ACM, Philadelphia, January 2022. https:\/\/doi.org\/10.1145\/3497775.3503694","DOI":"10.1145\/3497775.3503694"},{"key":"7_CR16","doi-asserted-by":"publisher","unstructured":"Guilloud, S., Pit-Claudel, C.: Verified and optimized implementation of orthologic proof search. In: Piskac, R., Rakamaric, Z. (eds.) Computer Aided Verification - 37th International Conference, CAV 2025, July 23-25, 2025, Proceedings, Part III. LNCS, vol. 15933, pp. 130\u2013152. Springer, Zagreb, Croatia (2025). https:\/\/doi.org\/10.1007\/978-3-031-98682-6_8","DOI":"10.1007\/978-3-031-98682-6_8"},{"key":"7_CR17","doi-asserted-by":"publisher","unstructured":"Hamza, J., Voirol, N., Kuncak, V.: System FR: formalized foundations for the Stainless verifier. Proc. ACM Program. Lang. 3(OOPSLA), 166:1\u2013166:30 (2019). https:\/\/doi.org\/10.1145\/3360592","DOI":"10.1145\/3360592"},{"key":"7_CR18","doi-asserted-by":"publisher","unstructured":"Huet, G.: The zipper. J. Functional Programm. 7(5), 549\u2013554 (1997). https:\/\/doi.org\/10.1017\/S0956796897002864","DOI":"10.1017\/S0956796897002864"},{"key":"7_CR19","unstructured":"Java microbenchmark harness (JMH). https:\/\/github.com\/openjdk\/jmh. Retrieved 25 January 2026"},{"key":"7_CR20","unstructured":"Leroy, X.: The CompCert C verified compiler: Documentation and user\u2019s manual. report, Inria, December 2024. https:\/\/inria.hal.science\/hal-01091802, pages: 1"},{"key":"7_CR21","unstructured":"Leroy, X., Blazy, S., K\u00e4stner, D., Schommer, B., Pister, M., Ferdinand, C.: CompCert - a formally verified optimizing compiler. In: ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress, SEE, HAL, Toulouse, France, January 2016. https:\/\/inria.hal.science\/hal-01238879"},{"key":"7_CR22","doi-asserted-by":"publisher","unstructured":"Li, A.W., Mamouras, K.: Efficient algorithms for the uniform tokenization problem. Proc. ACM Program. Lang. 9(OOPSLA1), 1492\u20131518 (2025). https:\/\/doi.org\/10.1145\/3720498","DOI":"10.1145\/3720498"},{"key":"7_CR23","doi-asserted-by":"publisher","unstructured":"Madhavan, R., Kulal, S., Kuncak, V.: Contract-based resource verification for higher-order functions with memoization. SIGPLAN Not. 52(1), 330\u2013343 (2017). https:\/\/doi.org\/10.1145\/3093333.3009874","DOI":"10.1145\/3093333.3009874"},{"key":"7_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BFb0055126","volume-title":"Theorem Proving in Higher Order Logics","author":"T Nipkow","year":"1998","unstructured":"Nipkow, T.: Verified lexical analysis. In: Grundy, J., Newey, M. (eds.) TPHOLs 1998. LNCS, vol. 1479, pp. 1\u201315. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0055126"},{"key":"7_CR25","unstructured":"OCamllex. https:\/\/ocaml.org\/manual\/5.3\/lexyacc.html. retrieved 15 May 2026"},{"key":"7_CR26","unstructured":"Ouedraogo, W., Scherer, G., Strassburger, L.: Coqlex artifact gitlab repository. https:\/\/gitlab.inria.fr\/wouedrao\/coqlex\/-\/tree\/master\/Comparison\/JSON?ref_type=heads, December 2023"},{"key":"7_CR27","doi-asserted-by":"publisher","unstructured":"Ouedraogo, W., Scherer, G., Strassburger, L.: Coqlex: generating formally verified lexers. Art Sci. Eng. Programm. 8(1), 3\u20131 (2023). https:\/\/doi.org\/10.22152\/programming-journal.org\/2024\/8\/3","DOI":"10.22152\/programming-journal.org\/2024\/8\/3"},{"key":"7_CR28","doi-asserted-by":"publisher","unstructured":"Owens, S., Reppy, J., Turon, A.: Regular-expression derivatives re-examined. J. Funct. Program. 19(2), 173\u2013190 (2009). https:\/\/doi.org\/10.1017\/S0956796808007090","DOI":"10.1017\/S0956796808007090"},{"key":"7_CR29","unstructured":"Paxson, V., et\u00a0al.: Flex\u2013fast lexical analyzer generator. Lawrence Berkeley Laboratory (1995)"},{"key":"7_CR30","unstructured":"Ranta, A.: Grammatical Framework - Programming with Multilingual Grammars. CSLI Studies in Computational Linguistics, Cambridge University Press (2011). http:\/\/cslipublications.stanford.edu\/site\/9781575866277.shtml"},{"key":"7_CR31","doi-asserted-by":"publisher","unstructured":"Rendel, T., Ostermann, K.: Invertible syntax descriptions: unifying parsing and pretty printing. SIGPLAN Not. 45(11), 1\u201312 (2010). https:\/\/doi.org\/10.1145\/2088456.1863525","DOI":"10.1145\/2088456.1863525"},{"key":"7_CR32","doi-asserted-by":"publisher","unstructured":"Reps, T.W.: \u201cMaximal-munch\u201d tokenization in linear time. ACM Trans. Program. Lang. Syst. 20(2), 259\u2013273 (1998). https:\/\/doi.org\/10.1145\/276393.276394","DOI":"10.1145\/276393.276394"},{"key":"7_CR33","doi-asserted-by":"publisher","unstructured":"Santo, N.D., Barri\u00e8re, A., Pit-Claudel, C.: A Coq mechanization of JavaScript regular expression semantics. Proc. ACM Program. Lang. 8(ICFP), 1003\u20131031 (2024). https:\/\/doi.org\/10.1145\/3674666","DOI":"10.1145\/3674666"},{"key":"7_CR34","unstructured":"epfl-lara\/stainless. https:\/\/github.com\/epfl-lara\/stainless, May 2026, original-date: 2016-08-17T14:08:38Z"},{"key":"7_CR35","doi-asserted-by":"publisher","unstructured":"Varatalu, I.E., Veanes, M., Ernits, J.: Re#: High performance derivative-based regex matching with intersection, complement, and restricted lookarounds. Proc. ACM Programm. Lang. 9(POPL), 1\u201332 (2025). https:\/\/doi.org\/10.1145\/3704837","DOI":"10.1145\/3704837"},{"key":"7_CR36","doi-asserted-by":"publisher","unstructured":"W\u00fcrthinger, T., et al.: Practical partial evaluation for high-performance dynamic language runtimes. In: Cohen, A., Vechev, M.T. (eds.) Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017, Barcelona, Spain, June 18-23, 2017, pp. 662\u2013676. ACM (2017). https:\/\/doi.org\/10.1145\/3062341.3062381","DOI":"10.1145\/3062341.3062381"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-32526-6_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T08:44:35Z","timestamp":1784796275000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-32526-6_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032325259","9783032325266"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-32526-6_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"24 July 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","label":"Disclosure of Interests","group":{"name":"EthicsHeading","label":"Ethics"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Lisbon","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 July 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 July 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"38","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.floc26.org\/program","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}