{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:59:18Z","timestamp":1750309158603,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":28,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,10,19]],"date-time":"2023-10-19T00:00:00Z","timestamp":1697673600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF (National Science Foundation)","doi-asserted-by":"publisher","award":["1736209"],"award-info":[{"award-number":["1736209"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"NSF (National Science Foundation) SHF","doi-asserted-by":"publisher","award":["2007718"],"award-info":[{"award-number":["2007718"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2023,10,19]]},"DOI":"10.1145\/3623506.3623574","type":"proceedings-article","created":{"date-parts":[[2023,10,19]],"date-time":"2023-10-19T13:38:41Z","timestamp":1697722721000},"page":"1-13","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Thorium: A Language for Bounded Verification of Dynamic Reactive Objects"],"prefix":"10.1145","author":[{"given":"Kevin","family":"Baldor","sequence":"first","affiliation":[{"name":"University of Texas at San Antonio, San Antonio, USA \/ Southwest Research Institute, San Antonio, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xiaoyin","family":"Wang","sequence":"additional","affiliation":[{"name":"University of Texas at San Antonio, San Antonio, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jianwei","family":"Niu","sequence":"additional","affiliation":[{"name":"University of Texas at San Antonio, San Antonio, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,10,19]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01782772"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/SKG49510.2019.00034"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10617-017-9182-z"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(92)90005-V"},{"key":"e_1_3_2_1_5_1","unstructured":"Stephen Blackheath. 2016 (accessed 9 January 2017). Sodium. https:\/\/github.com\/SodiumFRP\/sodium \t\t\t\t  Stephen Blackheath. 2016 (accessed 9 January 2017). Sodium. https:\/\/github.com\/SodiumFRP\/sodium"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/41625.41641"},{"key":"e_1_3_2_1_7_1","unstructured":"The Qt Company. 2022. Qt|Cross-platform software for embedded and desktop. http:\/\/qt.io \t\t\t\t  The Qt Company. 2022. Qt|Cross-platform software for embedded and desktop. http:\/\/qt.io"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2007.70707"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/368273.368557"},{"key":"e_1_3_2_1_10_1","volume-title":"International Workshop on Verification, Model Checking, and Abstract Interpretation. 169\u2013185","author":"Dimitrova Rayna","year":"2012","unstructured":"Rayna Dimitrova , Bernd Finkbeiner , M\u00e1t\u00e9 Kov\u00e1cs , Markus N Rabe , and Helmut Seidl . 2012 . Model checking information flow in reactive systems . In International Workshop on Verification, Model Checking, and Abstract Interpretation. 169\u2013185 . Rayna Dimitrova, Bernd Finkbeiner, M\u00e1t\u00e9 Kov\u00e1cs, Markus N Rabe, and Helmut Seidl. 2012. Model checking information flow in reactive systems. In International Workshop on Verification, Model Checking, and Abstract Interpretation. 169\u2013185."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660193.2660240"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/258949.258973"},{"key":"e_1_3_2_1_13_1","volume-title":"International Conference on Computer Aided Verification. 1\u201316","author":"Halbwachs Nicolas","year":"1998","unstructured":"Nicolas Halbwachs . 1998 . Synchronous programming of reactive systems . In International Conference on Computer Aided Verification. 1\u201316 . Nicolas Halbwachs. 1998. Synchronous programming of reactive systems. In International Conference on Computer Aided Verification. 1\u201316."},{"volume-title":"Algebraic Methodology and Software Technology (AMAST\u201993)","author":"Halbwachs Nicolas","key":"e_1_3_2_1_14_1","unstructured":"Nicolas Halbwachs , Fabienne Lagnier , and Pascal Raymond . 1994. Synchronous observers and the verification of reactive systems . In Algebraic Methodology and Software Technology (AMAST\u201993) . Springer , 83\u201396. Nicolas Halbwachs, Fabienne Lagnier, and Pascal Raymond. 1994. Synchronous observers and the verification of reactive systems. In Algebraic Methodology and Software Technology (AMAST\u201993). Springer, 83\u201396."},{"key":"e_1_3_2_1_15_1","unstructured":"Philipp Haller and Stephen Tu. (accessed 6 Mar 2023). Scala Actors API. https:\/\/docs.scala-lang.org\/overviews\/core\/actors.html \t\t\t\t  Philipp Haller and Stephen Tu. (accessed 6 Mar 2023). Scala Actors API. https:\/\/docs.scala-lang.org\/overviews\/core\/actors.html"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(87)90035-9"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/1624775.1624804"},{"key":"e_1_3_2_1_18_1","unstructured":"Inc. Itemis. 2023. Itemis CREATE - state machines made easy. https:\/\/www.itemis.com\/en\/products\/itemis-create\/ \t\t\t\t  Inc. Itemis. 2023. Itemis CREATE - state machines made easy. https:\/\/www.itemis.com\/en\/products\/itemis-create\/"},{"key":"e_1_3_2_1_19_1","unstructured":"Inc. Itemis. (Last updated 2021). Yakindu. https:\/\/github.com\/Yakindu\/statecharts \t\t\t\t  Inc. Itemis. (Last updated 2021). Yakindu. https:\/\/github.com\/Yakindu\/statecharts"},{"key":"e_1_3_2_1_20_1","volume-title":"Software Abstractions: Logic, Language, and Analysis","author":"Jackson Daniel","year":"2006","unstructured":"Daniel Jackson . 2006 . Software Abstractions: Logic, Language, and Analysis . The MIT Press . isbn:0262101149 Daniel Jackson. 2006. Software Abstractions: Logic, Language, and Analysis. The MIT Press. isbn:0262101149"},{"key":"e_1_3_2_1_21_1","volume-title":"Proceedings of the sixth workshop on Programming languages meets program verification. 49\u201360","author":"Jeffrey Alan","year":"2012","unstructured":"Alan Jeffrey . 2012 . LTL types FRP: linear-time temporal logic propositions as types, proofs as functional reactive programs . In Proceedings of the sixth workshop on Programming languages meets program verification. 49\u201360 . Alan Jeffrey. 2012. LTL types FRP: linear-time temporal logic propositions as types, proofs as functional reactive programs. In Proceedings of the sixth workshop on Programming languages meets program verification. 49\u201360."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/5.97301"},{"key":"e_1_3_2_1_23_1","unstructured":"Inc Lightbend. 2011-2023(accessed 6 Mar 2023). Akka: build concurrent distributed and resilient message-driven applications for Java and Scala. https:\/\/akka.io\/ \t\t\t\t  Inc Lightbend. 2011-2023(accessed 6 Mar 2023). Akka: build concurrent distributed and resilient message-driven applications for Java and Scala. https:\/\/akka.io\/"},{"key":"e_1_3_2_1_24_1","volume-title":"I\u00f1igo Incer Romeo and Alberto Sangiovanni-Vincentelli.","author":"Patricia Derler Jeronimo Castrillon Andr\u00e9s Goens","year":"2019","unstructured":"Andr\u00e9s Goens Patricia Derler Jeronimo Castrillon Edward A. Lee Marten Lohstroh , I\u00f1igo Incer Romeo and Alberto Sangiovanni-Vincentelli. 2019 . Reactors : A Deterministic Model for Composable Reactive Systems. In Model-Based Design of Cyber Physical Systems (CyPhy) . https:\/\/www.icyphy.org\/publications\/2019_LohstrohEtAl3\/ Andr\u00e9s Goens Patricia Derler Jeronimo Castrillon Edward A. Lee Marten Lohstroh, I\u00f1igo Incer Romeo and Alberto Sangiovanni-Vincentelli. 2019. Reactors: A Deterministic Model for Composable Reactive Systems. In Model-Based Design of Cyber Physical Systems (CyPhy). https:\/\/www.icyphy.org\/publications\/2019_LohstrohEtAl3\/"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1900160.1900173"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2642937.2642938"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"crossref","unstructured":"Guido Salvaneschi Gerold Hintz and Mira Mezini. 2014. REScala: bridging between object-oriented and functional style in reactive applications. In MODULARITY. \t\t\t\t  Guido Salvaneschi Gerold Hintz and Mira Mezini. 2014. REScala: bridging between object-oriented and functional style in reactive applications. In MODULARITY.","DOI":"10.1145\/2577080.2577083"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-67067-2_19"}],"event":{"name":"REBLS '23: 10th ACM SIGPLAN International Workshop on Reactive and Event-Based Languages and Systems","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGAda ACM Special Interest Group on Ada Programming Language"],"location":"Cascais Portugal","acronym":"REBLS '23"},"container-title":["Proceedings of the 10th ACM SIGPLAN International Workshop on Reactive and Event-Based Languages and Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3623506.3623574","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3623506.3623574","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T22:51:01Z","timestamp":1750287061000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3623506.3623574"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,10,19]]},"references-count":28,"alternative-id":["10.1145\/3623506.3623574","10.1145\/3623506"],"URL":"https:\/\/doi.org\/10.1145\/3623506.3623574","relation":{},"subject":[],"published":{"date-parts":[[2023,10,19]]},"assertion":[{"value":"2023-10-19","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}