{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,12]],"date-time":"2026-02-12T11:36:28Z","timestamp":1770896188985,"version":"3.50.1"},"reference-count":56,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2020,1,30]],"date-time":"2020-01-30T00:00:00Z","timestamp":1580342400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Softw. Eng. Methodol."],"published-print":{"date-parts":[[2020,1,31]]},"abstract":"<jats:p>We introduce two complementary approaches to monitor decentralized systems. The first approach relies on systems with a centralized specification, i.e., when the specification is written for the behavior of the entire system. To do so, our approach introduces a data structure that (i) keeps track of the execution of an automaton (ii) has predictable parameters and size, and (iii) guarantees strong eventual consistency. The second approach defines decentralized specifications wherein multiple specifications are provided for separate parts of the system. We study two properties of decentralized specifications pertaining to monitorability and compatibility between specification and architecture. We also present a general algorithm for monitoring decentralized specifications. We map three existing algorithms to our approaches and provide a framework for analyzing their behavior. Furthermore, we present THEMIS, a framework for designing such decentralized algorithms and simulating their behavior. We demonstrate the usage of THEMIS to compare multiple algorithms and validate the trends predicted by the analysis in two scenarios: a synthetic benchmark and the Chiron user interface.<\/jats:p>","DOI":"10.1145\/3355181","type":"journal-article","created":{"date-parts":[[2020,1,30]],"date-time":"2020-01-30T22:27:53Z","timestamp":1580423273000},"page":"1-57","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":19,"title":["On the Monitoring of Decentralized Specifications"],"prefix":"10.1145","volume":"29","author":[{"given":"Antoine","family":"El-Hokayem","sequence":"first","affiliation":[{"name":"Univ. Grenoble Alpes, CNRS, Grenoble INP, VERIMAG, Grenoble, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0114-0641","authenticated-orcid":false,"given":"Yli\u00e8s","family":"Falcone","sequence":"additional","affiliation":[{"name":"Univ. Grenoble Alpes, CNRS, Inria, Grenoble INP, LIG, Grenoble, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2020,1,30]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"1999. Patterns Project. http:\/\/patterns.projects.cs.ksu.edu.  1999. Patterns Project. http:\/\/patterns.projects.cs.ksu.edu."},{"key":"e_1_2_1_2_1","unstructured":"1999. Patterns Project: List of specifications. http:\/\/patterns.projects.cs.ksu.edu\/documentation\/specifications\/AFTER.raw.  1999. Patterns Project: List of specifications. http:\/\/patterns.projects.cs.ksu.edu\/documentation\/specifications\/AFTER.raw."},{"key":"e_1_2_1_3_1","volume-title":"Siegel","author":"Avrunin George S.","year":"1999","unstructured":"George S. Avrunin , James C. Corbett , Matthew B. Dwyer , Corina S. Pasareanu , and Stephen F . Siegel . 1999 . Comparing Finite-State Verification Techniques for Concurrent Software. Technical Report. University of Massachusetts , Amherst. George S. Avrunin, James C. Corbett, Matthew B. Dwyer, Corina S. Pasareanu, and Stephen F. Siegel. 1999. Comparing Finite-State Verification Techniques for Concurrent Software. Technical Report. University of Massachusetts, Amherst."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.124.9"},{"key":"e_1_2_1_5_1","volume-title":"Lecture Notes in Computer Science","volume":"10457","author":"Bartocci Ezio","year":"2018","unstructured":"Ezio Bartocci and Yli\u00e8s Falcone ( Eds .). 2018 . Lectures on Runtime Verification\u2014Introductory and Advanced Topics . Lecture Notes in Computer Science , Vol. 10457 . Springer. DOI:https:\/\/doi.org\/10.1007\/978-3-319-75632-5 10.1007\/978-3-319-75632-5 Ezio Bartocci and Yli\u00e8s Falcone (Eds.). 2018. Lectures on Runtime Verification\u2014Introductory and Advanced Topics. Lecture Notes in Computer Science, Vol. 10457. Springer. DOI:https:\/\/doi.org\/10.1007\/978-3-319-75632-5"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-017-0454-5"},{"key":"e_1_2_1_7_1","volume-title":"Proceedings of the 35th IARCS Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS\u201915)","volume":"45","author":"Basin David A.","year":"2015","unstructured":"David A. Basin , Felix Klaedtke , and Eugen Zalinescu . 2015 . Failure-aware runtime verification of distributed systems . In Proceedings of the 35th IARCS Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS\u201915) . LIPIcs, Prahladh Harsha and G. Ramalingam (Eds.) , Vol. 45 . Schloss Dagstuhl\u2014Leibniz-Zentrum fuer Informatik, 590--603. DOI:https:\/\/doi.org\/10.4230\/LIPIcs.FSTTCS.2015.590 10.4230\/LIPIcs.FSTTCS.2015.590 David A. Basin, Felix Klaedtke, and Eugen Zalinescu. 2015. Failure-aware runtime verification of distributed systems. In Proceedings of the 35th IARCS Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS\u201915). LIPIcs, Prahladh Harsha and G. Ramalingam (Eds.), Vol. 45. Schloss Dagstuhl\u2014Leibniz-Zentrum fuer Informatik, 590--603. DOI:https:\/\/doi.org\/10.4230\/LIPIcs.FSTTCS.2015.590"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-016-0253-8"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2000799.2000800"},{"key":"e_1_2_1_10_1","series-title":"Lecture Notes in Computer Science, Dimitra Giannakopoulou and Dominique M\u00e9ry (Eds.)","volume-title":"FM 2012: - 18th Proceedings of the 18th International Symposium on Formal Methods","author":"Bauer Andreas Klaus","unstructured":"Andreas Klaus Bauer and Yli\u00e8s Falcone . 2012. Decentralised LTL monitoring . In FM 2012: - 18th Proceedings of the 18th International Symposium on Formal Methods . Lecture Notes in Computer Science, Dimitra Giannakopoulou and Dominique M\u00e9ry (Eds.) , Vol. 7436 . Springer , 85--100. DOI:https:\/\/doi.org\/10.1007\/978-3-642-32759-9_10 10.1007\/978-3-642-32759-9_10 Andreas Klaus Bauer and Yli\u00e8s Falcone. 2012. Decentralised LTL monitoring. In FM 2012: - 18th Proceedings of the 18th International Symposium on Formal Methods. Lecture Notes in Computer Science, Dimitra Giannakopoulou and Dominique M\u00e9ry (Eds.), Vol. 7436. Springer, 85--100. DOI:https:\/\/doi.org\/10.1007\/978-3-642-32759-9_10"},{"key":"#cr-split#-e_1_2_1_11_1.1","doi-asserted-by":"crossref","unstructured":"Borzoo Bonakdarpour Pierre Fraigniaud Sergio Rajsbaum and Corentin Travers. 2016. Challenges in fault-tolerant distributed runtime verification. See Reference Margaria and Steffen [39] 363--370. DOI:https:\/\/doi.org\/10.1007\/978-3-319-47169-3_27 10.1007\/978-3-319-47169-3_27","DOI":"10.1007\/978-3-319-47169-3_27"},{"key":"#cr-split#-e_1_2_1_11_1.2","doi-asserted-by":"crossref","unstructured":"Borzoo Bonakdarpour Pierre Fraigniaud Sergio Rajsbaum and Corentin Travers. 2016. Challenges in fault-tolerant distributed runtime verification. See Reference Margaria and Steffen [39] 363--370. DOI:https:\/\/doi.org\/10.1007\/978-3-319-47169-3_27","DOI":"10.1007\/978-3-319-47169-3_27"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70575-8_3"},{"key":"e_1_2_1_13_1","unstructured":"CERN. 1999. http:\/\/dst.lbl.gov\/ACSSoftware\/colt\/. http:\/\/dst.lbl.gov\/ACSSoftware\/colt\/.  CERN. 1999. http:\/\/dst.lbl.gov\/ACSSoftware\/colt\/. http:\/\/dst.lbl.gov\/ACSSoftware\/colt\/."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-11164-3_12"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-016-0251-x"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/HPCC.2012.220"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIME.2005.26"},{"key":"e_1_2_1_18_1","volume-title":"Formal Methods: Foundations and Applications, Simone Cavalheiro and Jos\u00e9 Fiadeiro (Eds.)","author":"Decker Normann","unstructured":"Normann Decker , Philip Gottschling , Christian Hochberger , Martin Leucker , Torben Scheffel , Malte Schmitz , and Alexander Weiss . 2017. Rapidly adjustable non-intrusive online monitoring for multi-core systems . In Formal Methods: Foundations and Applications, Simone Cavalheiro and Jos\u00e9 Fiadeiro (Eds.) . Springer International Publishing , Cham , 179--196. Normann Decker, Philip Gottschling, Christian Hochberger, Martin Leucker, Torben Scheffel, Malte Schmitz, and Alexander Weiss. 2017. Rapidly adjustable non-intrusive online monitoring for multi-core systems. In Formal Methods: Foundations and Applications, Simone Cavalheiro and Jos\u00e9 Fiadeiro (Eds.). Springer International Publishing, Cham, 179--196."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2014.02.052"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32621-9_5"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-02444-8_31"},{"key":"e_1_2_1_22_1","volume-title":"Proceedings of the International Conference on Software Engineering (ICSE\u201999)","author":"Dwyer Matthew B.","unstructured":"Matthew B. Dwyer , George S. Avrunin , and James C. Corbett . 1999. Patterns in property specifications for finite-state verification . In Proceedings of the International Conference on Software Engineering (ICSE\u201999) , Barry W. Boehm, David Garlan, and Jeff Kramer (Eds.). ACM, 411--420. DOI:https:\/\/doi.org\/10.1145\/302405.302672 10.1145\/302405.302672 Matthew B. Dwyer, George S. Avrunin, and James C. Corbett. 1999. Patterns in property specifications for finite-state verification. In Proceedings of the International Conference on Software Engineering (ICSE\u201999), Barry W. Boehm, David Garlan, and Jeff Kramer (Eds.). ACM, 411--420. DOI:https:\/\/doi.org\/10.1145\/302405.302672"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3092703.3092723"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3092703.3098224"},{"key":"e_1_2_1_25_1","unstructured":"Antoine El-Hokayem and Yli\u00e8s Falcone. 2017. THEMIS Website. https:\/\/gitlab.inria.fr\/monitoring\/themis.  Antoine El-Hokayem and Yli\u00e8s Falcone. 2017. THEMIS Website. https:\/\/gitlab.inria.fr\/monitoring\/themis."},{"key":"e_1_2_1_26_1","unstructured":"Antoine El-Hokayem and Yli\u00e8s Falcone. 2018. THEMIS Article Artifact. https:\/\/gitlab.inria.fr\/monitoring\/themis-artifact-article.  Antoine El-Hokayem and Yli\u00e8s Falcone. 2018. THEMIS Article Artifact. https:\/\/gitlab.inria.fr\/monitoring\/themis-artifact-article."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-16612-9_9"},{"key":"#cr-split#-e_1_2_1_28_1.1","doi-asserted-by":"crossref","unstructured":"Yli\u00e8s Falcone Tom Cornebize and Jean-Claude Fernandez. 2014. Efficient and generalized decentralized monitoring of regular languages. In Proceedings of the 34th Formal Techniques for Distributed Objects Components and Systems (IFIP WG 6.1 International Conference (FORTE'14) Held as Part of the 9th International Federated Conference on Distributed Computing Techniques (DisCoTec'14). Lecture Notes in Computer Science Erika \u00c1brah\u00e1m and Catuscia Palamidessi (Eds.) Vol. 8461. Springer 66--83. DOI:https:\/\/doi.org\/10.1007\/978-3-662-43613-4_5 10.1007\/978-3-662-43613-4_5","DOI":"10.1007\/978-3-662-43613-4_5"},{"key":"#cr-split#-e_1_2_1_28_1.2","doi-asserted-by":"crossref","unstructured":"Yli\u00e8s Falcone Tom Cornebize and Jean-Claude Fernandez. 2014. Efficient and generalized decentralized monitoring of regular languages. In Proceedings of the 34th Formal Techniques for Distributed Objects Components and Systems (IFIP WG 6.1 International Conference (FORTE'14) Held as Part of the 9th International Federated Conference on Distributed Computing Techniques (DisCoTec'14). Lecture Notes in Computer Science Erika \u00c1brah\u00e1m and Catuscia Palamidessi (Eds.) Vol. 8461. Springer 66--83. DOI:https:\/\/doi.org\/10.1007\/978-3-662-43613-4_5","DOI":"10.1007\/978-3-662-43613-4_5"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/3115971.3116162"},{"key":"e_1_2_1_30_1","volume-title":"A tutorial on runtime verification","author":"Falcone Yli\u00e8s","unstructured":"Yli\u00e8s Falcone , Klaus Havelund , and Giles Reger . 2013. A tutorial on runtime verification . In Engineering Dependable Software Systems, Manfred Broy, Doron A. Peled, and Georg Kalus (Eds.). NATO Science for Peace and Security Series, d: Information and Communication Security, Vol. 34 . IOS Press , 141--175. DOI:https:\/\/doi.org\/10.3233\/978-1-61499-207-3-141 10.3233\/978-1-61499-207-3-141 Yli\u00e8s Falcone, Klaus Havelund, and Giles Reger. 2013. A tutorial on runtime verification. In Engineering Dependable Software Systems, Manfred Broy, Doron A. Peled, and Georg Kalus (Eds.). NATO Science for Peace and Security Series, d: Information and Communication Security, Vol. 34. IOS Press, 141--175. DOI:https:\/\/doi.org\/10.3233\/978-1-61499-207-3-141"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-03769-7_14"},{"key":"#cr-split#-e_1_2_1_32_1.1","doi-asserted-by":"crossref","unstructured":"Yli\u00e8s Falcone Leonardo Mariani Antoine Rollet and Saikat Saha. 2018. Runtime failure prevention and reaction. See Reference Bartocci and Falcone [5] 103--134. DOI:https:\/\/doi.org\/10.1007\/978-3-319-75632-5_4 10.1007\/978-3-319-75632-5_4","DOI":"10.1007\/978-3-319-75632-5_4"},{"key":"#cr-split#-e_1_2_1_32_1.2","doi-asserted-by":"crossref","unstructured":"Yli\u00e8s Falcone Leonardo Mariani Antoine Rollet and Saikat Saha. 2018. Runtime failure prevention and reaction. See Reference Bartocci and Falcone [5] 103--134. DOI:https:\/\/doi.org\/10.1007\/978-3-319-75632-5_4","DOI":"10.1007\/978-3-319-75632-5_4"},{"key":"#cr-split#-e_1_2_1_33_1.1","doi-asserted-by":"crossref","unstructured":"Adrian Francalanza Jorge A. P\u00e9rez and C\u00e9sar S\u00e1nchez. 2018. Runtime verification for decentralised and distributed systems. See Reference Bartocci and Falcone [5] 176--210. DOI:https:\/\/doi.org\/10.1007\/978-3-319-75632-5_6 10.1007\/978-3-319-75632-5_6","DOI":"10.1007\/978-3-319-75632-5_6"},{"key":"#cr-split#-e_1_2_1_33_1.2","doi-asserted-by":"crossref","unstructured":"Adrian Francalanza Jorge A. P\u00e9rez and C\u00e9sar S\u00e1nchez. 2018. Runtime verification for decentralised and distributed systems. See Reference Bartocci and Falcone [5] 176--210. DOI:https:\/\/doi.org\/10.1007\/978-3-319-75632-5_6","DOI":"10.1007\/978-3-319-75632-5_6"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-46982-9_6"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-67531-2_22"},{"key":"e_1_2_1_36_1","volume-title":"Griswold","author":"Kiczales Gregor","year":"2001","unstructured":"Gregor Kiczales , Erik Hilsdale , Jim Hugunin , Mik Kersten , Jeffrey Palm , and William G . Griswold . 2001 . An overview of AspectJ. In Proceedings of the ECOOP 2001 - Object-Oriented Programming, 15th European Conference. Lecture Notes in Computer Science, J\u00f8rgen Lindskov Knudsen (Ed.), Vol. 2072 . Springer , 327--353. DOI:https:\/\/doi.org\/10.1007\/3-540-45337-7_18 10.1007\/3-540-45337-7_18 Gregor Kiczales, Erik Hilsdale, Jim Hugunin, Mik Kersten, Jeffrey Palm, and William G. Griswold. 2001. An overview of AspectJ. In Proceedings of the ECOOP 2001 - Object-Oriented Programming, 15th European Conference. Lecture Notes in Computer Science, J\u00f8rgen Lindskov Knudsen (Ed.), Vol. 2072. Springer, 327--353. DOI:https:\/\/doi.org\/10.1007\/3-540-45337-7_18"},{"key":"e_1_2_1_37_1","volume-title":"Proceedings of the 11th Euromicro Conference on Real-Time Systems (ECRTS\u201999)","author":"Kim Moonjoo","year":"1999","unstructured":"Moonjoo Kim , Mahesh Viswanathan , Han\u00eane Ben-Abdallah , Sampath Kannan , Insup Lee , and Oleg Sokolsky . 1999 . Formally specified monitoring of temporal properties . In Proceedings of the 11th Euromicro Conference on Real-Time Systems (ECRTS\u201999) . IEEE Computer Society, 114--122. DOI:https:\/\/doi.org\/10.1109\/EMRTS. 1999.777457 10.1109\/EMRTS.1999.777457 Moonjoo Kim, Mahesh Viswanathan, Han\u00eane Ben-Abdallah, Sampath Kannan, Insup Lee, and Oleg Sokolsky. 1999. Formally specified monitoring of temporal properties. In Proceedings of the 11th Euromicro Conference on Real-Time Systems (ECRTS\u201999). IEEE Computer Society, 114--122. DOI:https:\/\/doi.org\/10.1109\/EMRTS.1999.777457"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2008.08.004"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-47169-3_29"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/IPDPS.2015.95"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2015.12.037"},{"key":"e_1_2_1_42_1","volume-title":"Proceedings of the 21st International Symposium on Distributed Computing (DISC\u201907)","volume":"4731","author":"Vinit","unstructured":"Vinit A. Ogale and Vijay K. Garg. 2007. Detecting temporal logic predicates on distributed computations . In Proceedings of the 21st International Symposium on Distributed Computing (DISC\u201907) . Lecture Notes in Computer Science, Andrzej Pelc (Ed.) , Vol. 4731 . Springer, 420--434. DOI:https:\/\/doi.org\/10.1007\/978-3-540-75142-7_32 10.1007\/978-3-540-75142-7_32 Vinit A. Ogale and Vijay K. Garg. 2007. Detecting temporal logic predicates on distributed computations. In Proceedings of the 21st International Symposium on Distributed Computing (DISC\u201907). Lecture Notes in Computer Science, Andrzej Pelc (Ed.), Vol. 4731. Springer, 420--434. DOI:https:\/\/doi.org\/10.1007\/978-3-540-75142-7_32"},{"key":"e_1_2_1_43_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the 14th International Symposium on Formal Methods","author":"Pnueli Amir","unstructured":"Amir Pnueli and Aleksandr Zaks . 2006. PSL model checking and run-time verification via testers . In Proceedings of the 14th International Symposium on Formal Methods . Lecture Notes in Computer Science , Jayadev Misra, Tobias Nipkow, and Emil Sekerinski (Eds.), Vol. 4085 . Springer , 573--586. DOI:https:\/\/doi.org\/10.1007\/11813040_38 10.1007\/11813040_38 Amir Pnueli and Aleksandr Zaks. 2006. PSL model checking and run-time verification via testers. In Proceedings of the 14th International Symposium on Formal Methods. Lecture Notes in Computer Science, Jayadev Misra, Tobias Nipkow, and Emil Sekerinski (Eds.), Vol. 4085. Springer, 573--586. DOI:https:\/\/doi.org\/10.1007\/11813040_38"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10515-005-6205-y"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2014.6961843"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.5555\/998675.999446"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24550-3_29"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1137\/0201010"},{"key":"e_1_2_1_49_1","unstructured":"The Chiron Team. 1999. Chiron User Interface. http:\/\/laser.cs.umass.edu\/verification-examples\/chiron\/index.html.  The Chiron Team. 1999. Chiron User Interface. http:\/\/laser.cs.umass.edu\/verification-examples\/chiron\/index.html."},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.5555\/2773579.2773774"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/79173.79181"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/12485.12491"}],"container-title":["ACM Transactions on Software Engineering and Methodology"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3355181","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3355181","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:44:42Z","timestamp":1750203882000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3355181"}},"subtitle":["Semantics, Properties, Analysis, and Simulation"],"short-title":[],"issued":{"date-parts":[[2020,1,30]]},"references-count":56,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2020,1,31]]}},"alternative-id":["10.1145\/3355181"],"URL":"https:\/\/doi.org\/10.1145\/3355181","relation":{},"ISSN":["1049-331X","1557-7392"],"issn-type":[{"value":"1049-331X","type":"print"},{"value":"1557-7392","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,1,30]]},"assertion":[{"value":"2018-04-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-07-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2020-01-30","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}