{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,12]],"date-time":"2026-06-12T04:35:11Z","timestamp":1781238911633,"version":"3.54.1"},"publisher-location":"Cham","reference-count":56,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031906428","type":"print"},{"value":"9783031906435","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T00:00:00Z","timestamp":1746057600000},"content-version":"vor","delay-in-days":120,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Mission-time Linear Temporal Logic (MLTL), a widely used subset of popular specification logics like STL and MTL, is often used to model and verify real world systems in safety-critical contexts. As the results of formal verification are only as trustworthy as their input specifications, the WEST tool was created to facilitate writing MLTL specifications. Accordingly, it is vital to demonstrate that WEST itself works correctly. To that end, we verify the WEST algorithm, which converts MLTL formulas to (logically equivalent) regular expressions, in the theorem prover Isabelle\/HOL. Our top-level result establishes the correctness of the regular expression transformation; we then generate a code export from our verified development and use this to experimentally validate the existing WEST tool. To facilitate this, we develop some verified support for checking the equivalence of two regular expressions.<\/jats:p>","DOI":"10.1007\/978-3-031-90643-5_13","type":"book-chapter","created":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T06:08:33Z","timestamp":1745993313000},"page":"254-275","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Formally Verifying a Transformation from MLTL Formulas to Regular Expressions"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1730-6180","authenticated-orcid":false,"given":"Zili","family":"Wang","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9336-6006","authenticated-orcid":false,"given":"Katherine","family":"Kosaian","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6718-2828","authenticated-orcid":false,"given":"Kristin Yvonne","family":"Rozier","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,5,1]]},"reference":[{"key":"13_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R., Henzinger, T.A.: Real-time Logics: Complexity and Expressiveness. In: LICS. pp. 390\u2013401. IEEE (1990)","DOI":"10.1109\/LICS.1990.113764"},{"key":"13_CR2","doi-asserted-by":"publisher","unstructured":"Alur, R., Feder, T., Henzinger, T.A.: The Benefits of Relaxing Punctuality. In: Logrippo, L. (ed.) Proceedings of the Tenth Annual ACM Symposium on Principles of Distributed Computing, Montreal, Quebec, Canada, August 19-21, 1991. pp. 139\u2013152. ACM (1991). https:\/\/doi.org\/10.1145\/112600.112613, https:\/\/doi.org\/10.1145\/112600.112613","DOI":"10.1145\/112600.112613"},{"key":"13_CR3","unstructured":"Amjad, R., van Glabbeek, R., O\u2019Connor, L.: Definitive set semantics for LTL3. Archive of Formal Proofs (August 2024), https:\/\/isa-afp.org\/entries\/LTL3_Semantics.html, Formal proof development"},{"key":"13_CR4","unstructured":"Anastasia Mavridou: Capturing and Analyzing Requirements with FRET. Presentation, nasa formal methods symposium, https:\/\/github.com\/NASA-SW-VnV\/fret, National Aeronautics and Space Agency, Pasadena, California, USA (May 2022)"},{"key":"13_CR5","doi-asserted-by":"publisher","unstructured":"Aurandt, A., Jones, P., Rozier, K.Y.: Runtime Verification Triggers Real-time, Autonomous Fault Recovery on the CySat-I. In: Proceedings of the 14th NASA Formal Methods Symposium (NFM 2022). Lecture Notes in Computer Science (LNCS), vol. 13260. Springer, Cham, Caltech, California, USA (May 2022). https:\/\/doi.org\/10.1007\/978-3-031-06773-0_45","DOI":"10.1007\/978-3-031-06773-0_45"},{"key":"13_CR6","doi-asserted-by":"publisher","unstructured":"Ballarin, C.: Locales and locale expressions in Isabelle\/Isar. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES. LNCS, vol.\u00a03085, pp. 34\u201350. Springer (2003). https:\/\/doi.org\/10.1007\/978-3-540-24849-1_3, https:\/\/doi.org\/10.1007\/978-3-540-24849-1_3","DOI":"10.1007\/978-3-540-24849-1_3"},{"key":"13_CR7","doi-asserted-by":"publisher","unstructured":"Ballarin, C.: Locales: A module system for mathematical theories. J. Autom. Reason. 52(2), 123\u2013153 (2014). https:\/\/doi.org\/10.1007\/S10817-013-9284-7, https:\/\/doi.org\/10.1007\/s10817-013-9284-7","DOI":"10.1007\/S10817-013-9284-7"},{"key":"13_CR8","doi-asserted-by":"publisher","unstructured":"Basin, D.A., Dardinier, T., Hauser, N., Heimes, L., y\u00a0Munive, J.J.H., Kaletsch, N., Krstic, S., Marsicano, E., Raszyk, M., Schneider, J., Tirore, D.L., Traytel, D., Zingg, S.: VeriMon: A formally verified monitoring tool. In: Seidl, H., Liu, Z., Pasareanu, C.S. (eds.) ICTAC. LNCS, vol. 13572, pp.\u00a01\u20136. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-17715-6_1, https:\/\/doi.org\/10.1007\/978-3-031-17715-6_1","DOI":"10.1007\/978-3-031-17715-6_1"},{"key":"13_CR9","doi-asserted-by":"publisher","unstructured":"Cavada, R., Cimatti, A., Dorigatti, M., Griggio, A., Mariotti, A., Micheli, A., Mover, S., Roveri, M., Tonetta, S.: The nuXmv symbolic model checker. In: Biere, A., Bloem, R. (eds.) CAV. LNCS, vol.\u00a08559, pp. 334\u2013342. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_22, https:\/\/doi.org\/10.1007\/978-3-319-08867-9_22","DOI":"10.1007\/978-3-319-08867-9_22"},{"key":"13_CR10","doi-asserted-by":"publisher","unstructured":"Chattopadhyay, A., Mamouras, K.: A Verified Online Monitor for Metric Temporal Logic with Quantitative Semantics. In: Runtime Verification: 20th International Conference, RV 2020, Los Angeles, CA, USA, October 6\u20139, 2020, Proceedings. p. 383\u2013403. Springer-Verlag, Berlin, Heidelberg (2020). https:\/\/doi.org\/10.1007\/978-3-030-60508-7_21, https:\/\/doi.org\/10.1007\/978-3-030-60508-7_21","DOI":"10.1007\/978-3-030-60508-7_21"},{"key":"13_CR11","doi-asserted-by":"crossref","unstructured":"Chattopadhyay, A., Mamouras, K.: A verified online monitor for metric temporal logic with quantitative semantics. In: Deshmukh, J., Ni\u010dkovi\u0107, D. (eds.) Runtime Verification. pp. 383\u2013403. Springer International Publishing, Cham (2020)","DOI":"10.1007\/978-3-030-60508-7_21"},{"key":"13_CR12","doi-asserted-by":"publisher","unstructured":"Conrad, E., Titolo, L., Giannakopoulou, D., Pressburger, T., Dutle, A.: A compositional proof framework for FRETish requirements. In: Popescu, A., Zdancewic, S. (eds.) CPP \u201922: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Philadelphia, PA, USA, January 17 - 18, 2022. pp. 68\u201381. ACM (2022). https:\/\/doi.org\/10.1145\/3497775.3503685, https:\/\/doi.org\/10.1145\/3497775.3503685","DOI":"10.1145\/3497775.3503685"},{"key":"13_CR13","doi-asserted-by":"publisher","unstructured":"Coquand, T., Siles, V.: A Decision Procedure for Regular Expression Equivalence in Type Theory. In: Jouannaud, J., Shao, Z. (eds.) CPP. LNCS, vol.\u00a07086, pp. 119\u2013134. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-25379-9_11, https:\/\/doi.org\/10.1007\/978-3-642-25379-9_11","DOI":"10.1007\/978-3-642-25379-9_11"},{"key":"13_CR14","doi-asserted-by":"publisher","unstructured":"Coupet-Grimal, S.: An axiomatization of linear temporal logic in the calculus of inductive constructions. J. Log. Comput. 13(6), 801\u2013813 (2003). https:\/\/doi.org\/10.1093\/LOGCOM\/13.6.801, https:\/\/doi.org\/10.1093\/logcom\/13.6.801","DOI":"10.1093\/LOGCOM\/13.6.801"},{"key":"13_CR15","doi-asserted-by":"publisher","unstructured":"Dabney, J.B., Badger, J.M., Rajagopal, P.: Adding a verification view for an autonomous real-time system architecture. In: Proceedings of SciTech Forum. p. Online. 2021-0566, AIAA (January 2021). https:\/\/doi.org\/10.2514\/6.2021-0566","DOI":"10.2514\/6.2021-0566"},{"key":"13_CR16","unstructured":"Dabney, J.B., Rajagopal, P., Badger, J.M.: Using assume-guarantee contracts for developmental verification of autonomous spacecraft. Flight Software Workshop (FSW) Online: https:\/\/www.youtube.com\/watch?v=HFnn6TzblPg (February 2022)"},{"key":"13_CR17","doi-asserted-by":"publisher","unstructured":"Elwing, J., Gamboa-Guzman, L., Sorkin, J., Travesset, C., Wang, Z., Rozier, K.Y.: Mission-time LTL (MLTL) formula validation via regular expressions. In: Herber, P., Wijs, A. (eds.) iFM. LNCS, vol. 14300, pp. 279\u2013301. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-47705-8_15, https:\/\/doi.org\/10.1007\/978-3-031-47705-8_15","DOI":"10.1007\/978-3-031-47705-8_15"},{"key":"13_CR18","doi-asserted-by":"crossref","unstructured":"Esparza, J., Lammich, P., Neumann, R., Nipkow, T., Schimpf, A., Smaus, J.G.: A fully verified executable LTL model checker. Archive of Formal Proofs (May 2014), https:\/\/isa-afp.org\/entries\/CAVA_LTL_Modelchecker.html, Formal proof development","DOI":"10.1007\/978-3-642-39799-8_31"},{"key":"13_CR19","unstructured":"Giannakopoulou, D., Mavridou, A., Rhein, J., Pressburger, T., Schumann, J., Shi, N.: Formal requirements elicitation with FRET. In: International Working Conference on Requirements Engineering: Foundation for Software Quality (REFSQ-2020). No. ARC-E-DAA-TN77785 (2020)"},{"key":"13_CR20","unstructured":"Haftmann, F.: Code generation from specifications in higher-order logic. Ph.D. thesis, Technical University Munich (2009), http:\/\/mediatum2.ub.tum.de\/node?id=886023"},{"key":"13_CR21","doi-asserted-by":"publisher","unstructured":"Hariharan, G., Jones, P.H., Rozier, K.Y., Wongpiromsarn, T.: Maximum satisfiability of Mission-time Linear Temporal Logic. In: Petrucci, L., Sproston, J. (eds.) FORMATS. LNCS, vol. 14138, pp. 86\u2013104. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-42626-1_6, https:\/\/doi.org\/10.1007\/978-3-031-42626-1_6","DOI":"10.1007\/978-3-031-42626-1_6"},{"key":"13_CR22","doi-asserted-by":"publisher","unstructured":"Hupel, L., Nipkow, T.: A Verified Compiler from Isabelle\/HOL to CakeML. In: Ahmed, A. (ed.) ESOP. LNCS, vol. 10801, pp. 999\u20131026. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-89884-1_35, https:\/\/doi.org\/10.1007\/978-3-319-89884-1_35","DOI":"10.1007\/978-3-319-89884-1_35"},{"key":"13_CR23","doi-asserted-by":"crossref","unstructured":"Johannsen, C., Jones, P., Kempa, B., Rozier, K.Y., Zhang, P.: R2U2 Version 3.0: Re-Imagining a Toolchain for Specification, Resource Estimation, and Optimized Observer Generation for Runtime Verification in Hardware and Software. In: Enea, C., Lal, A. (eds.) Computer Aided Verification. pp. 483\u2013497. Springer Nature Switzerland, Cham (2023)","DOI":"10.1007\/978-3-031-37709-9_23"},{"key":"13_CR24","doi-asserted-by":"crossref","unstructured":"Kempa, B., Zhang, P., Jones, P.H., Zambreno, J., Rozier, K.Y.: Embedding Online Runtime Verification for Fault Disambiguation on Robonaut2. In: FORMATS. pp. 196\u2013214. LNCS, Springer, Vienna, Austria (September 2020), http:\/\/research.temporallogic.org\/papers\/KZJZR20.pdf","DOI":"10.1007\/978-3-030-57628-8_12"},{"key":"13_CR25","unstructured":"Kessler, F.B.: nuXmv 1.1.0 (2016-05-10) Release Notes. https:\/\/es-static.fbk.eu\/tools\/nuxmv\/downloads\/NEWS.txt (2016)"},{"key":"13_CR26","unstructured":"Kosaian, K., Wang, Z., Sloan, E.: Mission-time linear temporal logic. Archive of Formal Proofs (January 2025), https:\/\/isa-afp.org\/entries\/Mission_Time_LTL.html, Formal proof development"},{"key":"13_CR27","unstructured":"Kosaian, K., Wang, Z., Sloan, E., Rozier, K.: Formalizing MLTL formula progression in Isabelle\/HOL (2024), https:\/\/arxiv.org\/abs\/2410.03465"},{"key":"13_CR28","doi-asserted-by":"crossref","unstructured":"Krauss, A.: Automating Recursive Definitions and Termination Proofs in Higher-Order Logic. Ph.D. thesis, Technische Universit\u00e4t M\u00fcnchen (2009)","DOI":"10.1007\/s10817-009-9157-2"},{"key":"13_CR29","doi-asserted-by":"publisher","unstructured":"Krauss, A., Nipkow, T.: Proof Pearl: Regular Expression Equivalence and Relation Algebra. J. Autom. Reason. 49(1), 95\u2013106 (2012). https:\/\/doi.org\/10.1007\/S10817-011-9223-4, https:\/\/doi.org\/10.1007\/s10817-011-9223-4","DOI":"10.1007\/S10817-011-9223-4"},{"key":"13_CR30","doi-asserted-by":"crossref","unstructured":"Li, J., Vardi, M.Y., Rozier, K.Y.: Satisfiability Checking for Mission-Time LTL. In: Proceedings of 31st International Conference on Computer Aided Verification (CAV 2019). LNCS, Springer, New York, NY, USA (July 2019)","DOI":"10.1007\/978-3-030-25543-5_1"},{"key":"13_CR31","doi-asserted-by":"publisher","unstructured":"Luppen, Z., Jacks, M., Baughman, N., Hertz, B., Cutler, J., Lee, D.Y., Rozier, K.Y.: Elucidation and Analysis of Specification Patterns in Aerospace System Telemetry. In: Proceedings of the 14th NASA Formal Methods Symposium (NFM 2022). Lecture Notes in Computer Science (LNCS), vol. 13260. Springer, Cham, Caltech, California, USA (May 2022). https:\/\/doi.org\/10.1007\/978-3-031-06773-0_28","DOI":"10.1007\/978-3-031-06773-0_28"},{"key":"13_CR32","doi-asserted-by":"crossref","unstructured":"Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems, pp. 152\u2013166. Springer (2004)","DOI":"10.1007\/978-3-540-30206-3_12"},{"key":"13_CR33","unstructured":"Marlow, S., Jones, S.L.P.: The Glasgow Haskell Compiler (2012), https:\/\/api.semanticscholar.org\/CorpusID:35370"},{"key":"13_CR34","unstructured":"NASA Technology Transfer Program: FRET : Formal Requirements Elicitation Tool (ARC-18066-1). Online: https:\/\/software.nasa.gov\/software\/ARC-18066-1 (2024)"},{"key":"13_CR35","unstructured":"Perez, I.: Runtime verification with ogma. In: Invited Talk to University of California (2023)"},{"key":"13_CR36","unstructured":"Perez, I., Goodloe, A.: OGMA. https:\/\/github.com\/nasa\/ogma (2021)"},{"key":"13_CR37","doi-asserted-by":"crossref","unstructured":"Perez, I., Mavridou, A., Pressburger, T., Goodloe, A., Giannakopoulou, D.: Automated translation of natural language requirements to runtime monitors. In: Fisman, D., Rosu, G. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. pp. 387\u2013395. Springer International Publishing, Cham (2022)","DOI":"10.1007\/978-3-030-99524-9_21"},{"key":"13_CR38","doi-asserted-by":"publisher","unstructured":"Pnueli, A., Arons, T.: TLPVS: A PVS-based LTL verification system. In: Dershowitz, N. (ed.) Verification: Theory and Practice, Essays Dedicated to Zohar Manna on the Occasion of His 64th Birthday. LNCS, vol.\u00a02772, pp. 598\u2013625. Springer (2003). https:\/\/doi.org\/10.1007\/978-3-540-39910-0_26, https:\/\/doi.org\/10.1007\/978-3-540-39910-0_26","DOI":"10.1007\/978-3-540-39910-0_26"},{"key":"13_CR39","doi-asserted-by":"crossref","unstructured":"Raszyk, M., Basin, D., Traytel, D.: Multi-head monitoring of metric dynamic logic. In: International Symposium on Automated Technology for Verification and Analysis. pp. 233\u2013250. Springer (2020)","DOI":"10.1007\/978-3-030-59152-6_13"},{"key":"13_CR40","doi-asserted-by":"crossref","unstructured":"Reinbacher, T., Rozier, K.Y., Schumann, J.: Temporal-logic based runtime observer pairs for system health management of real-time systems. In: Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Lecture Notes in Computer Science (LNCS), vol.\u00a08413, pp. 357\u2013372. Springer-Verlag (April 2014)","DOI":"10.1007\/978-3-642-54862-8_24"},{"key":"13_CR41","doi-asserted-by":"publisher","unstructured":"Roohi, N., Viswanathan, M.: Revisiting MITL to fix decision procedures. In: Dillig, I., Palsberg, J. (eds.) VMCAI. LNCS, vol. 10747, pp. 474\u2013494. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-73721-8_22, https:\/\/doi.org\/10.1007\/978-3-319-73721-8_22","DOI":"10.1007\/978-3-319-73721-8_22"},{"key":"13_CR42","doi-asserted-by":"publisher","unstructured":"Rozier, K.Y.: Specification: The biggest bottleneck in formal methods and autonomy. In: Proceedings of 8th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2016). LNCS, vol.\u00a09971, pp. 1\u201319. Springer-Verlag, Toronto, ON, Canada (July 2016). https:\/\/doi.org\/10.1007\/978-3-319-48869-1_2","DOI":"10.1007\/978-3-319-48869-1_2"},{"key":"13_CR43","unstructured":"Rozier, K.Y., Schumann, J.: R2U2: Tool Overview. In: Proceedings of International Workshop on Competitions, Usability, Benchmarks, Evaluation, and Standardisation for Runtime Verification Tools (RV-CUBES). vol.\u00a03, pp. 138\u2013156. Kalpa Publications, Seattle, WA, USA (September 2017), https:\/\/easychair.org\/publications\/paper\/Vncw"},{"key":"13_CR44","unstructured":"Schimpf, A., Lammich, P.: Converting linear-time temporal logic to generalized B\u00fcchi automata. Archive of Formal Proofs (May 2014), https:\/\/isa-afp.org\/entries\/LTL_to_GBA.html, Formal proof development"},{"key":"13_CR45","unstructured":"Seidl, B., Sickert, S.: A compositional and unified translation of LTL into $$\\omega $$-automata. Archive of Formal Proofs (April 2019), https:\/\/isa-afp.org\/entries\/LTL_Master_Theorem.html, Formal proof development"},{"key":"13_CR46","unstructured":"Sickert, S.: Converting linear temporal logic to deterministic (generalized) Rabin automata. Archive of Formal Proofs (September 2015), https:\/\/isa-afp.org\/entries\/LTL_to_DRA.html, Formal proof development"},{"key":"13_CR47","unstructured":"Sickert, S.: Linear temporal logic. Archive of Formal Proofs (March 2016), https:\/\/isa-afp.org\/entries\/LTL.html, Formal proof development"},{"key":"13_CR48","doi-asserted-by":"crossref","unstructured":"Sickert, S.: An efficient normalisation procedure for linear temporal logic: Isabelle\/HOL formalisation. Archive of Formal Proofs (May 2020), https:\/\/isa-afp.org\/entries\/LTL_Normal_Form.html, Formal proof development","DOI":"10.1145\/3373718.3394743"},{"key":"13_CR49","unstructured":"Tilscher, S., Wimmer, S.: LL(1) parser generator. Archive of Formal Proofs (May 2024), https:\/\/isa-afp.org\/entries\/LL1_Parser.html, formal proof development"},{"key":"13_CR50","unstructured":"Titolo, L., Conrad, E., Giannakopoulou, D., Pressburger, T., Dutle, A.: FRET Proof Framework. https:\/\/lauratitolo.github.io\/project\/fret-proof-framework\/ (2022)"},{"key":"13_CR51","unstructured":"Wang, Z., Gamboa-Guzman, L.P., Rozier, K.Y.: WEST: Interactive Validation of Mission-time Linear Temporal Logic (MLTL) (2024), https:\/\/temporallogic.org\/research\/WEST\/"},{"key":"13_CR52","unstructured":"Wang, Z., Kosaian, K.: Mission-time linear temporal logic to regular expressions. Archive of Formal Proofs (January 2025), https:\/\/isa-afp.org\/entries\/Mission_Time_LTL_to_Regular_Expression.html, Formal proof development"},{"key":"13_CR53","unstructured":"Wang, Z., Kosaian, K., Rozier, K.Y.: Formally verifying a transformation from MLTL formulas to regular expressions (2025), https:\/\/arxiv.org\/abs\/2501.17444"},{"key":"13_CR54","doi-asserted-by":"crossref","unstructured":"Wu, C., Zhang, X., Urban, C.: A formalisation of the Myhill-Nerode theorem based on regular expressions (proof pearl). In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) Interactive Theorem Proving. pp. 341\u2013356. Springer Berlin Heidelberg, Berlin, Heidelberg (2011)","DOI":"10.1007\/978-3-642-22863-6_25"},{"key":"13_CR55","doi-asserted-by":"publisher","unstructured":"Zhang, P., Aurandt, A.A., Dureja, R., Jones, P.H., Rozier, K.Y.: Model predictive runtime verification for cyber-physical systems with real-time deadlines. In: Petrucci, L., Sproston, J. (eds.) Formal Modeling and Analysis of Timed Systems - 21st International Conference, FORMATS 2023, Antwerp, Belgium, September 19-21, 2023, Proceedings. Lecture Notes in Computer Science, vol. 14138, pp. 158\u2013180. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-42626-1_10, https:\/\/doi.org\/10.1007\/978-3-031-42626-1_10","DOI":"10.1007\/978-3-031-42626-1_10"},{"key":"13_CR56","doi-asserted-by":"publisher","unstructured":"Zhuchko, E., Veanes, M., Ebner, G.: Lean formalization of extended regular expression matching with lookarounds. In: Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs. p. 118\u2013131. CPP 2024, Association for Computing Machinery, New York, NY, USA (2024). https:\/\/doi.org\/10.1145\/3636501.3636959, https:\/\/doi.org\/10.1145\/3636501.3636959","DOI":"10.1145\/3636501.3636959"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-90643-5_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T06:08:54Z","timestamp":1745993334000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-90643-5_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031906428","9783031906435"],"references-count":56,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-90643-5_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"1 May 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hamilton, ON","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 May 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 May 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2025\/conferences\/tacas\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}