{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T13:16:21Z","timestamp":1782911781214,"version":"3.54.5"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032227485","type":"print"},{"value":"9783032227492","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:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-22749-2_2","type":"book-chapter","created":{"date-parts":[[2026,4,15]],"date-time":"2026-04-15T13:10:26Z","timestamp":1776258626000},"page":"23-41","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Efficient Verification of Lingua Franca Programs"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0708-3721","authenticated-orcid":false,"given":"Peter Csaba","family":"\u00d6lveczky","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4055-8714","authenticated-orcid":false,"given":"Mario","family":"Reja","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3519-1057","authenticated-orcid":false,"given":"Mikheil","family":"Rukhaia","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6430-5175","authenticated-orcid":false,"given":"Kyungmin","family":"Bae","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9324-9838","authenticated-orcid":false,"given":"Mircea","family":"Marin","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,4,15]]},"reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"Aceto, L., Cimini, M., Ing\u00f3lfsd\u00f3ttir, A., Reynisson, A.H., Sigurdarson, S.H., Sirjani, M.: Modelling and simulation of asynchronous real-time systems using Timed Rebeca. In: FOCLASA. EPTCS, vol.\u00a058, pp. 1\u201319 (2011)","DOI":"10.4204\/EPTCS.58.1"},{"key":"2_CR2","doi-asserted-by":"crossref","unstructured":"Bae, K., Olarte, C., \u00d6lveczky, P.C.: Modeling and analyzing real-time systems in rewriting logic. In: Concurrent Programming, Open Systems and Formal Methods: Essays Dedicated to Gul Agha to Celebrate His Scientific Career. Lecture Notes in Computer Science, vol. 16120. Springer Nature Switzerland, Cham (2026)","DOI":"10.1007\/978-3-032-05291-9_21"},{"key":"2_CR3","doi-asserted-by":"crossref","unstructured":"Bae, K., \u00d6lveczky, P.C., Feng, T.H., Lee, E.A., Tripakis, S.: Verifying hierarchical Ptolemy II discrete-event models using Real-Time Maude. Science of Computer Programming 77(12) (2012)","DOI":"10.1016\/j.scico.2010.10.002"},{"key":"2_CR4","unstructured":"Chen, P.W., Lin, S., Godbole, A., Singh, R., Polgreen, E., Lee, E., Seshia, S.: PolyVer: A compositional approach for polyglot system modeling and verification. In: Proceedings of the 25th Conference on Formal Methods in Computer-Aided Design \u2013 FMCAD 2025. TU Wien Academic Press (2025)"},{"key":"2_CR5","doi-asserted-by":"crossref","unstructured":"Chen, X., Ro\u015fu, G.: $$\\mathbb{K}$$\u2014a semantic framework for programming languages and formal analysis. In: SETSS. pp. 122\u2013158. Springer, Cham (2020)","DOI":"10.1007\/978-3-030-55089-9_4"},{"key":"2_CR6","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Meseguer, J., Lincoln, P., Mart\u0131-Oliet, N., Talcott, C.: All About Maude \u2013 A High-Performance Logical Framework, LNCS, vol.\u00a04350. Springer, Berlin, Heidelberg (2007)"},{"key":"2_CR7","doi-asserted-by":"crossref","unstructured":"Deantoni, J., Cambeiro, J., Bateni, S., Lin, S., Lohstroh, M.: Debugging and verification tools for Lingua Franca in Gemoc Studio. In: 2021 Forum on specification & Design Languages (FDL). pp. 01\u201308 (2021)","DOI":"10.1109\/FDL53530.2021.9568383"},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"Lepri, D., \u00c1brah\u00e1m, E., \u00d6lveczky, P.C.: Sound and complete timed CTL model checking of timed Kripke structures and real-time rewrite theories. Science of Computer Programming 99, 128\u2013192 (2015)","DOI":"10.1016\/j.scico.2014.06.006"},{"key":"2_CR9","doi-asserted-by":"crossref","unstructured":"Lin, S., Manerkar, Y.A., Lohstroh, M., Polgreen, E., Yu, S.J., Jerad, C., Lee, E.A., Seshia, S.A.: Towards Building Verifiable CPS using Lingua Franca. ACM Transactions on Embedded Computing Systems 22(5s), 1\u201324(2023)","DOI":"10.1145\/3609134"},{"key":"2_CR10","unstructured":"https:\/\/www.lf-lang.org\/, accessed October 16, 2025"},{"key":"2_CR11","unstructured":"Lohstroh, M.: Reactors: A Deterministic Model of Concurrent Computation for Reactive Systems. Ph.D. thesis, University of California, Berkeley (2020)"},{"key":"2_CR12","doi-asserted-by":"crossref","unstructured":"Lohstroh, M., Menard, C., Bateni, S., Lee, E.A.: Toward a Lingua Franca for Deterministic Concurrent Systems. ACM Transactions on Embedded Computing Systems (TECS) 20(4), 1\u201327 (2021)","DOI":"10.1145\/3448128"},{"key":"2_CR13","doi-asserted-by":"crossref","unstructured":"Marin, M., \u00d6lveczky, P.C., Reja, M., Rukhaia, M., Bae, K.: Semantics and formal analysis of Lingua Franca CPS specifications in rewriting logic. In: Rebeca for Actor Analysis in Action \u2013 Essays Dedicated to Marjan Sirjani on the Occasion of Her 60th Birthday, LNCS, vol. 15560. Springer (2025)","DOI":"10.1007\/978-3-031-85134-6_4"},{"key":"2_CR14","doi-asserted-by":"crossref","unstructured":"Menard, C., et\u00a0al.: High-performance deterministic concurrency using Lingua Franca. ACM Transactions on Architecture and Code Optimization 20(4), 1\u201329 (2023)","DOI":"10.1145\/3617687"},{"key":"2_CR15","doi-asserted-by":"crossref","unstructured":"Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theor. Comput. Sci. 96(1) (1992)","DOI":"10.1016\/0304-3975(92)90182-F"},{"key":"2_CR16","doi-asserted-by":"crossref","unstructured":"Meseguer, J., Rosu, G.: The rewriting logic semantics project. Theor. Comput. Sci. 373(3) (2007)","DOI":"10.1016\/j.tcs.2006.12.018"},{"key":"2_CR17","doi-asserted-by":"crossref","unstructured":"\u00d6lveczky, P.C.: Semantics, simulation, and formal analysis of modeling languages for embedded systems in Real-Time Maude. In: Formal Modeling: Actors, Open Systems, Biological Systems. LNCS, vol.\u00a07000. Springer (2011)","DOI":"10.1007\/978-3-642-24933-4_19"},{"key":"2_CR18","doi-asserted-by":"crossref","unstructured":"\u00d6lveczky, P.C.: Real-Time Maude and its applications. In: Proc. WRLA\u201914. LNCS, vol.\u00a08663. Springer (2014)","DOI":"10.1007\/978-3-319-12904-4_3"},{"key":"2_CR19","doi-asserted-by":"crossref","unstructured":"\u00d6lveczky, P.C., Meseguer, J.: Specification of real-time and hybrid systems in rewriting logic. Theor. Comput. Sci. 285(2), 359\u2013405 (2002)","DOI":"10.1016\/S0304-3975(01)00363-2"},{"key":"2_CR20","doi-asserted-by":"crossref","unstructured":"\u00d6lveczky, P.C., Reja, M., Rukhaia, M., Bae, K., Marin, M.: Efficient verification of Lingua Franca programs (longer report) (2025), available at https:\/\/the-mrd.github.io\/tacas-artifact","DOI":"10.1007\/978-3-032-22749-2_2"},{"key":"2_CR21","doi-asserted-by":"crossref","unstructured":"Rossel, M., Lin, S., Lohstroh, M., Castrill\u00f3n, J., Goens, A.: Provable determinism for software in cyber-physical systems. In: Verified Software. Theories, Tools and Experiments (VSTTE 2023). LNCS, vol. 14095. Springer (2023)","DOI":"10.1007\/978-3-031-66064-1_6"},{"key":"2_CR22","doi-asserted-by":"crossref","unstructured":"Sirjani, M., Lee, E.A., Khamespanah, E.: Verification of cyberphysical systems. Mathematics 8(7), \u00a01068 (2020)","DOI":"10.3390\/math8071068"}],"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-032-22749-2_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T00:30:41Z","timestamp":1782865841000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-22749-2_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032227485","9783032227492"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-22749-2_2","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":"15 April 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The Maude semantics of LF, case studies, benchmark examples, and scripts to reproduce the experimental results, together with the\n                      LF-mc\n                      tool, are available at\n                      \n                      .","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Data-Availability Statement"}},{"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":"Turin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","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":"11 April 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 April 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"32","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/about\/tacas\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}