{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:03:28Z","timestamp":1776305008357,"version":"3.50.1"},"reference-count":75,"publisher":"Association for Computing Machinery (ACM)","issue":"5s","license":[{"start":{"date-parts":[[2023,9,9]],"date-time":"2023-09-09T00:00:00Z","timestamp":1694217600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"National Science Foundation","award":["CNS-1836601, CNS-2233769"],"award-info":[{"award-number":["CNS-1836601, CNS-2233769"]}]},{"name":"iCyPhy Research Center"},{"name":"Denso, Siemens, and Toyota"},{"DOI":"10.13039\/100000185","name":"DARPA","doi-asserted-by":"crossref","award":["FA8750-20-C-0156"],"award-info":[{"award-number":["FA8750-20-C-0156"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2023,10,31]]},"abstract":"<jats:p>\n            Formal verification of cyber-physical systems (CPS) is challenging because it has to consider real-time and concurrency aspects that are often absent in ordinary software. Moreover, the software in CPS is often complex and low-level, making it hard to assure that a formal model of the system used for verification is a faithful representation of the actual implementation, which can undermine the value of a verification result. To address this problem, we propose a methodology for building verifiable CPS based on the principle that a formal model of the software can be derived\n            <jats:italic>automatically<\/jats:italic>\n            from its implementation. Our approach requires that the system implementation is specified in\n            <jats:sc>Lingua Franca<\/jats:sc>\n            (LF), a polyglot coordination language tailored for real-time, concurrent CPS, which we made amenable to the specification of safety properties via annotations in the code. The program structure and the deterministic semantics of LF enable automatic construction of formal axiomatic models directly from LF programs. The generated models are automatically checked using Bounded Model Checking (BMC) by the verification engine\n            <jats:sc>Uclid5<\/jats:sc>\n            using the\n            <jats:sc>Z3<\/jats:sc>\n            SMT solver. The proposed technique enables checking a well-defined fragment of Safety Metric Temporal Logic (Safety MTL) formulas. To ensure the completeness of BMC, we present a method to derive an upper bound on the completeness threshold of an axiomatic model based on the semantics of LF. We implement our approach in the LF V\n            <jats:sc>erifier<\/jats:sc>\n            and evaluate it using a benchmark suite with 22 programs sampled from real-life applications and benchmarks for Erlang, Lustre, actor-oriented languages, and RTOSes. The LF V\n            <jats:sc>erifier<\/jats:sc>\n            correctly checks 21 out of 22 programs automatically.\n          <\/jats:p>","DOI":"10.1145\/3609134","type":"journal-article","created":{"date-parts":[[2023,9,9]],"date-time":"2023-09-09T13:33:18Z","timestamp":1694266398000},"page":"1-24","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":10,"title":["Towards Building Verifiable CPS using Lingua Franca"],"prefix":"10.1145","volume":"22","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6885-5572","authenticated-orcid":false,"given":"Shaokai","family":"Lin","sequence":"first","affiliation":[{"name":"University of California, Berkeley, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6954-2292","authenticated-orcid":false,"given":"Yatin A.","family":"Manerkar","sequence":"additional","affiliation":[{"name":"University of Michigan, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8833-4117","authenticated-orcid":false,"given":"Marten","family":"Lohstroh","sequence":"additional","affiliation":[{"name":"University of California, Berkeley, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9032-7661","authenticated-orcid":false,"given":"Elizabeth","family":"Polgreen","sequence":"additional","affiliation":[{"name":"University of Edinburgh, Scotland"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2585-9586","authenticated-orcid":false,"given":"Sheng-Jung","family":"Yu","sequence":"additional","affiliation":[{"name":"University of California, Berkeley, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5442-3098","authenticated-orcid":false,"given":"Chadlia","family":"Jerad","sequence":"additional","affiliation":[{"name":"University of Manouba, Tunisia"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5663-0584","authenticated-orcid":false,"given":"Edward A.","family":"Lee","sequence":"additional","affiliation":[{"name":"University of California, Berkeley, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6190-8707","authenticated-orcid":false,"given":"Sanjit A.","family":"Seshia","sequence":"additional","affiliation":[{"name":"University of California, Berkeley, USA"}]}],"member":"320","published-online":{"date-parts":[[2023,9,9]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1145\/2627752"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.5555\/2774947"},{"key":"e_1_3_2_4_2","first-page":"37","volume-title":"Syntax and Semantics of the Clock Constraint Specification Language (CCSL)","author":"Andr\u00e9 Charles","year":"2009","unstructured":"Charles Andr\u00e9. 2009. Syntax and Semantics of the Clock Constraint Specification Language (CCSL). Research Report RR-6925. INRIA. 37 pages. https:\/\/hal.inria.fr\/inria-00384077"},{"issue":"1","key":"e_1_3_2_5_2","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1007\/s10009-008-0091-0","article-title":"Bounded model checking of software using SMT solvers instead of SAT solvers","volume":"11","author":"Armando Alessandro","year":"2009","unstructured":"Alessandro Armando, Jacopo Mantovani, and Lorenzo Platania. 2009. Bounded model checking of software using SMT solvers instead of SAT solvers. International Journal on Software Tools for Technology Transfer 11, 1 (2009), 69\u201383.","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2004.12.021"},{"key":"e_1_3_2_7_2","first-page":"717","volume-title":"Formal Methods and Software Engineering","author":"Bae Kyungmin","year":"2009","unstructured":"Kyungmin Bae, Peter Csaba \u00d6lveczky, Thomas Huining Feng, and Stavros Tripakis. 2009. Verifying ptolemy II discrete-event models using real-time maude. In Formal Methods and Software Engineering, Karin Breitman and Ana Cavalcanti (Eds.). Springer, Berlin, 717\u2013736."},{"key":"e_1_3_2_8_2","first-page":"1267","volume-title":"Handbook of Satisfiability (2nd ed.)","author":"Barrett Clark","year":"2021","unstructured":"Clark Barrett, Roberto Sebastiani, Sanjit A. Seshia, and Cesare Tinelli. 2021. Satisfiability modulo theories. In Handbook of Satisfiability (2nd ed.), Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh (Eds.). IOS Press, Chapter 33, 1267\u20131329."},{"key":"e_1_3_2_9_2","article-title":"Xronos: Predictable coordination for safety-critical distributed embedded systems","author":"Bateni Soroush","year":"2022","unstructured":"Soroush Bateni, Marten Lohstroh, Hou Seng Wong, Rohan Tabish, Hokeun Kim, Shaokai Lin, Christian Menard, Cong Liu, and Edward A. Lee. 2022. Xronos: Predictable coordination for safety-critical distributed embedded systems. arXiv preprint arXiv:2207.09555 (2022).","journal-title":"arXiv preprint arXiv:2207.09555"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1109\/5.97297"},{"key":"e_1_3_2_11_2","volume-title":"Systems and Software Verification: Model-checking Techniques and Tools","author":"B\u00e9rard B\u00e9atrice","year":"2013","unstructured":"B\u00e9atrice B\u00e9rard, Michel Bidoit, Alain Finkel, Fran\u00e7ois Laroussinie, Antoine Petit, Laure Petrucci, and Philippe Schnoebelen. 2013. Systems and Software Verification: Model-checking Techniques and Tools. Springer Science & Business Media."},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.5555\/3074444"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.5555\/646483.691738"},{"issue":"99","key":"e_1_3_2_14_2","first-page":"457","article-title":"Bounded model checking.","volume":"185","author":"Biere Armin","year":"2009","unstructured":"Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Ofer Strichman, and Yunshan Zhu. 2009. Bounded model checking. Handbook of Satisfiability 185, 99 (2009), 457\u2013481.","journal-title":"Handbook of Satisfiability"},{"key":"e_1_3_2_15_2","doi-asserted-by":"crossref","unstructured":"Randal E. Bryant Shuvendu K. Lahiri and Sanjit A. Seshia. 2002. Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions(LNCS 2404) E. Brinksma and K. G. Larsen (Eds.). 78\u201392.","DOI":"10.1007\/3-540-45657-0_7"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-68612-7"},{"key":"e_1_3_2_17_2","first-page":"510","volume-title":"International Conference on Computer Aided Verification","author":"Champion Adrien","year":"2016","unstructured":"Adrien Champion, Alain Mebsout, Christoph Sticksel, and Cesare Tinelli. 2016. The kind 2 model checker. In International Conference on Computer Aided Verification. Springer, 510\u2013517."},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/359104.359108"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_3_2_20_2","first-page":"01","volume-title":"2021 Forum on Specification & Design Languages (FDL)","author":"Deantoni Julien","year":"2021","unstructured":"Julien Deantoni, Jo\u00e3o Cambeiro, Soroush Bateni, Shaokai Lin, and Marten Lohstroh. 2021. Debugging and verification tools for linga franca in GEMOC studio. In 2021 Forum on Specification & Design Languages (FDL). IEEE, 01\u201308."},{"key":"e_1_3_2_21_2","first-page":"23","volume-title":"Operational Semantics of the Model of Concurrency and Communication Language","author":"Deantoni Julien","year":"2014","unstructured":"Julien Deantoni, Papa Issa Diallo, Jo\u00ebl Champeau, Benoit Combemale, and Ciprian Teodorov. 2014. Operational Semantics of the Model of Concurrency and Communication Language. Research Report RR-8584. INRIA. 23 pages. https:\/\/hal.inria.fr\/hal-01060601"},{"key":"e_1_3_2_22_2","volume-title":"First Version Data Flow Procedure Language","author":"Dennis Jack B.","year":"1974","unstructured":"Jack B. Dennis. 1974. First Version Data Flow Procedure Language. Report MAC TM61. MIT Laboratory for Computer Science."},{"key":"e_1_3_2_23_2","doi-asserted-by":"crossref","first-page":"454","DOI":"10.1007\/978-3-642-38856-9_24","volume-title":"International Static Analysis Symposium","author":"D\u2019Osualdo Emanuele","year":"2013","unstructured":"Emanuele D\u2019Osualdo, Jonathan Kochems, and C.-H. Luke Ong. 2013. Automatic verification of erlang-style concurrency. In International Static Analysis Symposium. Springer, 454\u2013476."},{"key":"e_1_3_2_24_2","doi-asserted-by":"crossref","first-page":"603","DOI":"10.1007\/978-3-319-08867-9_40","volume-title":"International Conference on Computer Aided Verification","author":"Esparza Javier","year":"2014","unstructured":"Javier Esparza, Rusl\u00e1n Ledesma-Garza, Rupak Majumdar, Philipp Meyer, and Filip Niksic. 2014. An SMT-based approach to coverability analysis. In International Conference on Computer Aided Verification. Springer, 603\u2013619."},{"key":"e_1_3_2_25_2","unstructured":"Inc. Express Logic. [n. d.]. Measuring real-time performance of an RTOS."},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/1869542.1869625"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.265634"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.07.017"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1109\/MVT.2006.343641"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-012-0244-z"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2008.4484672"},{"key":"e_1_3_2_32_2","first-page":"331","volume-title":"Conference on Formal Methods in Computer-Aided Design\u2013Fmcad 2022","author":"Godbole Adwait","year":"2022","unstructured":"Adwait Godbole, Yatin A. Manerkar, and Sanjit A. Seshia. 2022. Automated conversion of axiomatic to operational models: Theory and practice. In Conference on Formal Methods in Computer-Aided Design\u2013Fmcad 2022. 331."},{"key":"e_1_3_2_33_2","first-page":"1","volume-title":"2008 Formal Methods in Computer-Aided Design","author":"Hagen George","year":"2008","unstructured":"George Hagen and Cesare Tinelli. 2008. Scaling up the formal verification of Lustre programs with SMT-based techniques. In 2008 Formal Methods in Computer-Aided Design. IEEE, 1\u20139."},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.159839"},{"key":"e_1_3_2_35_2","first-page":"166","volume-title":"EMSOFT 2001","author":"Henzinger T. A.","year":"2001","unstructured":"T. A. Henzinger, B. Horowitz, and C. M. Kirsch. 2001. Giotto: A time-triggered language for embedded programming. In EMSOFT 2001, Vol. LNCS 2211. Springer-Verlag, 166\u2013184."},{"key":"e_1_3_2_36_2","first-page":"235","volume-title":"Proceedings of the 3rd International Joint Conference on Artificial Intelligence. Standford, CA, USA, August 20-23, 1973","author":"Hewitt Carl","year":"1973","unstructured":"Carl Hewitt, Peter Boehler Bishop, and Richard Steiger. 1973. A universal modular ACTOR formalism for artificial intelligence. In Proceedings of the 3rd International Joint Conference on Artificial Intelligence. Standford, CA, USA, August 20-23, 1973. 235\u2013245."},{"key":"e_1_3_2_37_2","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1145\/2687357.2687368","volume-title":"Proceedings of the 4th International Workshop on Programming Based on Actors Agents & Decentralized Control","author":"Imam Shams M.","year":"2014","unstructured":"Shams M. Imam and Vivek Sarkar. 2014. Savina-an actor benchmark suite: Enabling empirical evaluation of actor libraries. In Proceedings of the 4th International Workshop on Programming Based on Actors Agents & Decentralized Control. 67\u201380."},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1145\/1141277.1141704"},{"key":"e_1_3_2_39_2","article-title":"An introductory lab in embedded and cyber-physical systems","author":"Jensen Jeff C.","year":"2012","unstructured":"Jeff C. Jensen, Edward A. Lee, and Sanjit A. Seshia. 2012. An introductory lab in embedded and cyber-physical systems. LeeSeshia.org, Berkeley, CA (2012).","journal-title":"LeeSeshia.org, Berkeley, CA"},{"key":"e_1_3_2_40_2","first-page":"471","volume-title":"Proc. of the IFIP Congress 74","author":"Kahn Gilles","year":"1974","unstructured":"Gilles Kahn. 1974. The semantics of a simple language for parallel programming. In Proc. of the IFIP Congress 74. North-Holland Publishing Co., 471\u2013475."},{"key":"e_1_3_2_41_2","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1007\/3-540-60360-3_42","volume-title":"Static Analysis","author":"Kobayashi Naoki","year":"1995","unstructured":"Naoki Kobayashi, Motoki Nakade, and Akinori Yonezawa. 1995. Static analysis of communication for asynchronous concurrent programming languages. In Static Analysis, Alan Mycroft (Ed.). Springer, Berlin, 225\u2013242."},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01995674"},{"key":"e_1_3_2_43_2","doi-asserted-by":"crossref","first-page":"298","DOI":"10.1007\/3-540-36384-X_24","volume-title":"International Workshop on Verification, Model Checking, and Abstract Interpretation","author":"Kroening Daniel","year":"2003","unstructured":"Daniel Kroening and Ofer Strichman. 2003. Efficient computation of recurrence diameters. In International Workshop on Verification, Model Checking, and Abstract Interpretation. Springer, 298\u2013309."},{"key":"e_1_3_2_44_2","doi-asserted-by":"crossref","first-page":"557","DOI":"10.1007\/978-3-642-22110-1_44","article-title":"Linear completeness thresholds for bounded model checking","author":"Kroening Daniel","year":"2011","unstructured":"Daniel Kroening, Ofer Strichman, Thomas Wahl, and James Worrell. 2011. Linear completeness thresholds for bounded model checking. Proceedings of the 23rd International Conference on Computer Aided Verification (CAV\u201911). 557\u2013572.","journal-title":"Proceedings of the 23rd International Conference on Computer Aided Verification (CAV\u201911)"},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_26"},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2009.88"},{"key":"e_1_3_2_47_2","doi-asserted-by":"crossref","unstructured":"Edward Lee and David Messerschmitt. 1987. Synchronous data flow. 75 9 (1987) 1235\u20131245.","DOI":"10.1109\/PROC.1987.13876"},{"key":"e_1_3_2_48_2","first-page":"363","volume-title":"2008 11th IEEE International Symposium on Object and Component-oriented Real-time Distributed Computing (ISORC)","author":"Lee Edward A.","year":"2008","unstructured":"Edward A. Lee. 2008. Cyber physical systems: Design challenges. In 2008 11th IEEE International Symposium on Object and Component-oriented Real-time Distributed Computing (ISORC). IEEE, 363\u2013369."},{"key":"e_1_3_2_49_2","article-title":"Quantifying and generalizing the CAP theorem","author":"Lee Edward A.","year":"2021","unstructured":"Edward A. Lee, Soroush Bateni, Shaokai Lin, Marten Lohstroh, and Christian Menard. 2021. Quantifying and generalizing the CAP theorem. arXiv:2109.07771 [cs.DC] (September 162021). https:\/\/arxiv.org\/abs\/2109.07771","journal-title":"arXiv:2109.07771 [cs.DC]"},{"key":"e_1_3_2_50_2","volume-title":"Introduction to Embedded Systems: A Cyber-physical Systems Approach","author":"Lee Edward Ashford","year":"2016","unstructured":"Edward Ashford Lee and Sanjit Arunkumar Seshia. 2016. Introduction to Embedded Systems: A Cyber-physical Systems Approach. Mit Press."},{"key":"e_1_3_2_51_2","article-title":"Reactors: A deterministic model for composable reactive systems","author":"Lohstroh Marten","year":"2019","unstructured":"Marten Lohstroh, I\u00f1igo Incer Romeo, Andr\u00e9s Goens, Patricia Derler, Jeronimo Castrillon, Edward A. Lee, and Alberto Sangiovanni-Vincentelli. 2019. Reactors: A deterministic model for composable reactive systems. Model-Based Design of Cyber Physical Systems (CyPhy\u201919) (2019).","journal-title":"Model-Based Design of Cyber Physical Systems (CyPhy\u201919)"},{"key":"e_1_3_2_52_2","doi-asserted-by":"publisher","DOI":"10.1145\/3448128"},{"key":"e_1_3_2_53_2","doi-asserted-by":"publisher","DOI":"10.1145\/3448128"},{"key":"e_1_3_2_54_2","doi-asserted-by":"publisher","DOI":"10.1109\/FDL50818.2020.9232939"},{"key":"e_1_3_2_55_2","doi-asserted-by":"publisher","DOI":"10.1145\/2980024.2872399"},{"key":"e_1_3_2_56_2","doi-asserted-by":"crossref","first-page":"4","DOI":"10.1007\/3-540-57318-6_22","volume-title":"Hybrid Systems","author":"Manna Zohar","year":"1993","unstructured":"Zohar Manna and Amir Pnueli. 1993. Verifying hybrid systems. In Hybrid Systems, Vol. LNCS 736. 4\u201335."},{"key":"e_1_3_2_57_2","unstructured":"DATE\u201920 Proceedings of the 2020 Design Automation and Test in Europe Conference (DATE) Christian Menard Andr\u00e9s Goens Marten Lohstroh Jeronimo Castrillon Achieving determinism in adaptive AUTOSAR 2020"},{"key":"e_1_3_2_58_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_21"},{"key":"e_1_3_2_59_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-8191(99)00070-8"},{"key":"e_1_3_2_60_2","doi-asserted-by":"crossref","first-page":"411","DOI":"10.1007\/11691372_27","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Ouaknine Jo\u00ebl","year":"2006","unstructured":"Jo\u00ebl Ouaknine and James Worrell. 2006. Safety metric temporal logic is fully decidable. In Tools and Algorithms for the Construction and Analysis of Systems, Holger Hermanns and Jens Palsberg (Eds.). Springer, Berlin, 411\u2013425."},{"key":"e_1_3_2_61_2","doi-asserted-by":"publisher","DOI":"10.2168\/lmcs-3(1:8)2007"},{"key":"e_1_3_2_62_2","article-title":"On the decidability and complexity of metric temporal logic over finite words","author":"Ouaknine Jo\u00ebl","year":"2007","unstructured":"Jo\u00ebl Ouaknine and James Worrell. 2007. On the decidability and complexity of metric temporal logic over finite words. arXiv preprint cs\/0702120 (2007).","journal-title":"arXiv preprint cs\/0702120"},{"key":"e_1_3_2_63_2","first-page":"1","volume-title":"International Conference on Formal Modeling and Analysis of Timed Systems","author":"Ouaknine Jo\u00ebl","year":"2008","unstructured":"Jo\u00ebl Ouaknine and James Worrell. 2008. Some recent results in metric temporal logic. In International Conference on Formal Modeling and Analysis of Timed Systems. Springer, 1\u201313."},{"key":"e_1_3_2_64_2","first-page":"1","article-title":"The definitive ANTLR 4 reference","author":"Parr Terence","year":"2013","unstructured":"Terence Parr. 2013. The definitive ANTLR 4 reference. The Definitive ANTLR 4 Reference (2013), 1\u2013326.","journal-title":"The Definitive ANTLR 4 Reference"},{"key":"e_1_3_2_65_2","doi-asserted-by":"crossref","first-page":"538","DOI":"10.1007\/978-3-031-13185-1_27","volume-title":"International Conference on Computer Aided Verification","author":"Polgreen Elizabeth","year":"2022","unstructured":"Elizabeth Polgreen, Kevin Cheang, Pranav Gaddamadugu, Adwait Godbole, Kevin Laeufer, Shaokai Lin, Yatin A. Manerkar, Federico Mora, and Sanjit A. Seshia. 2022. UCLID5: Multi-modal formal modeling, verification, and synthesis. In International Conference on Computer Aided Verification. Springer, 538\u2013551."},{"key":"e_1_3_2_66_2","doi-asserted-by":"publisher","DOI":"10.1145\/2491509.2491514"},{"key":"e_1_3_2_67_2","doi-asserted-by":"publisher","DOI":"10.1145\/1837274.1837461"},{"key":"e_1_3_2_68_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2014.01.008"},{"key":"e_1_3_2_69_2","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1145\/3337932.3338812","volume-title":"Proceedings of the Tenth ACM SIGPLAN Symposium on Scala","author":"Scalas Alceste","year":"2019","unstructured":"Alceste Scalas, Nobuko Yoshida, and Elias Benussi. 2019. Effpi: Verified message-passing programs in Dotty. In Proceedings of the Tenth ACM SIGPLAN Symposium on Scala. 27\u201331."},{"key":"e_1_3_2_70_2","article-title":"Modal reactors","author":"Schulz-Rosengarten Alexander","year":"2023","unstructured":"Alexander Schulz-Rosengarten, Reinhard von Hanxleden, Marten Lohstroh, Soroush Bateni, and Edward A. Lee. 2023. Modal reactors. arXiv preprint arXiv:2301.09597 (2023).","journal-title":"arXiv preprint arXiv:2301.09597"},{"key":"e_1_3_2_71_2","volume-title":"Proceedings of the 15th ACM\/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE)","author":"Seshia Sanjit A.","year":"2018","unstructured":"Sanjit A. Seshia and Pramod Subramanyan. 2018. UCLID5: Integrating modeling, verification, synthesis, and learning. In Proceedings of the 15th ACM\/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE)."},{"key":"e_1_3_2_72_2","doi-asserted-by":"publisher","DOI":"10.3390\/math8071068"},{"key":"e_1_3_2_73_2","unstructured":"Pramod Subramanyan and Sanjit A. Seshia. 2021. Getting started with Uclid5."},{"key":"e_1_3_2_74_2","doi-asserted-by":"crossref","first-page":"136","DOI":"10.1007\/978-3-319-66197-1_9","volume-title":"International Conference on Software Engineering and Formal Methods","author":"Wiik Jonatan","year":"2017","unstructured":"Jonatan Wiik and Pontus Bostr\u00f6m. 2017. Specification and automated verification of dynamic dataflow networks. In International Conference on Software Engineering and Formal Methods. Springer, 136\u2013151."},{"key":"e_1_3_2_75_2","volume-title":"Workshop on Programming based on Actors, Agents, and Decentralized Control (AGERE)","author":"Yasutake Shohei","year":"2015","unstructured":"Shohei Yasutake and Takuo Watanabe. 2015. Actario: A framework for reasoning about actor systems. In Workshop on Programming based on Actors, Agents, and Decentralized Control (AGERE)."},{"key":"e_1_3_2_76_2","doi-asserted-by":"publisher","DOI":"10.1063\/1.5012394"}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3609134","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3609134","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T17:48:58Z","timestamp":1750182538000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3609134"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,9,9]]},"references-count":75,"journal-issue":{"issue":"5s","published-print":{"date-parts":[[2023,10,31]]}},"alternative-id":["10.1145\/3609134"],"URL":"https:\/\/doi.org\/10.1145\/3609134","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"value":"1539-9087","type":"print"},{"value":"1558-3465","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,9,9]]},"assertion":[{"value":"2023-03-23","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-07-13","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-09-09","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}