{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,26]],"date-time":"2026-03-26T21:28:11Z","timestamp":1774560491869,"version":"3.50.1"},"reference-count":74,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2022,10,31]],"date-time":"2022-10-31T00:00:00Z","timestamp":1667174400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100001665","name":"Agence Nationale de la Recherche","doi-asserted-by":"publisher","award":["ANR-21-CE48-0011."],"award-info":[{"award-number":["ANR-21-CE48-0011."]}],"id":[{"id":"10.13039\/501100001665","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2022,10,31]]},"abstract":"<jats:p>This paper presents a Hoare-style calculus for formal reasoning about  \nreconfiguration programs of distributed systems. Such programs create  \nand delete components and\/or interactions (connectors) while the  \nsystem components change state according to their internal behaviour.  \nOur proof calculus uses a resource logic, in the spirit of Separation  \nLogic, to give local specifications of reconfiguration  \nactions. Moreover, distributed systems with an unbounded number of  \ncomponents are described using inductively defined predicates. The  \ncorrectness of reconfiguration programs relies on havoc invariants,  \nthat are assertions about the ongoing interactions in a part of the  \nsystem that is not affected by the structural change caused by the  \nreconfiguration. We present a proof system for such invariants in an  \nassume\/rely-guarantee style. We illustrate the feasibility of our  \napproach by proving the correctness of real-life distributed systems  \nwith reconfigurable (self-adjustable) tree architectures.<\/jats:p>","DOI":"10.1145\/3563293","type":"journal-article","created":{"date-parts":[[2022,10,31]],"date-time":"2022-10-31T20:23:35Z","timestamp":1667247815000},"page":"145-174","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Reasoning about distributed reconfigurable systems"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6394-3351","authenticated-orcid":false,"given":"Emma","family":"Ahrens","sequence":"first","affiliation":[{"name":"RWTH Aachen University, Aachen, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4412-5684","authenticated-orcid":false,"given":"Marius","family":"Bozga","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Grenoble Alpes, France \/ CNRS, France \/ Grenoble INP, France \/ VERIMAG, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3204-3294","authenticated-orcid":false,"given":"Radu","family":"Iosif","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Grenoble Alpes, France \/ CNRS, France \/ Grenoble INP, France \/ VERIMAG, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6143-1926","authenticated-orcid":false,"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[{"name":"RWTH Aachen University, Aachen, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,10,31]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"13th International Conference, TACAS 2007, Orna Grumberg and Michael Huth (Eds.) (LNCS","volume":"736","author":"Abdulla Parosh Aziz","year":"2007","unstructured":"Parosh Aziz Abdulla , Giorgio Delzanno , Noomene Ben Henda , and Ahmed Rezine . 2007 . Regular Model Checking Without Transducers (On Efficient Verification of Parameterized Systems). In Tools and Algorithms for the Construction and Analysis of Systems , 13th International Conference, TACAS 2007, Orna Grumberg and Michael Huth (Eds.) (LNCS , Vol. 4424). Springer, 721\u2013 736 . Parosh Aziz Abdulla, Giorgio Delzanno, Noomene Ben Henda, and Ahmed Rezine. 2007. Regular Model Checking Without Transducers (On Efficient Verification of Parameterized Systems). In Tools and Algorithms for the Construction and Analysis of Systems, 13th International Conference, TACAS 2007, Orna Grumberg and Michael Huth (Eds.) (LNCS, Vol. 4424). Springer, 721\u2013736."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2015.340"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129504004153"},{"key":"e_1_2_1_5_1","first-page":"143","article-title":"On Formal Properties of Simple Phrase Structure Grammars","volume":"14","author":"Bar-Hillel Yehoshua","year":"1961","unstructured":"Yehoshua Bar-Hillel , Micha Perles , and Eli Shamir . 1961 . On Formal Properties of Simple Phrase Structure Grammars . Sprachtypologie und Universalienforschung , 14 (1961), 143 \u2013 172 . Yehoshua Bar-Hillel, Micha Perles, and Eli Shamir. 1961. On Formal Properties of Simple Phrase Structure Grammars. Sprachtypologie und Universalienforschung, 14 (1961), 143\u2013172.","journal-title":"Sprachtypologie und Universalienforschung"},{"key":"e_1_2_1_6_1","volume-title":"Modeling Heterogeneous Real-time Components in BIP. In Fourth IEEE International Conference on Software Engineering and Formal Methods (SEFM","author":"Basu Ananda","year":"2006","unstructured":"Ananda Basu , Marius Bozga , and Joseph Sifakis . 2006 . Modeling Heterogeneous Real-time Components in BIP. In Fourth IEEE International Conference on Software Engineering and Formal Methods (SEFM 2006). IEEE Computer Society, 3\u201312. Ananda Basu, Marius Bozga, and Joseph Sifakis. 2006. Modeling Heterogeneous Real-time Components in BIP. In Fourth IEEE International Conference on Software Engineering and Formal Methods (SEFM 2006). IEEE Computer Society, 3\u201312."},{"key":"e_1_2_1_7_1","volume-title":"Decidability of Parameterized Verification","author":"Bloem Roderick","unstructured":"Roderick Bloem , Swen Jacobs , Ayrat Khalimov , Igor Konnov , Sasha Rubin , Helmut Veith , and Josef Widder . 2015. Decidability of Parameterized Verification . Morgan & Claypool Publishers . Roderick Bloem, Swen Jacobs, Ayrat Khalimov, Igor Konnov, Sasha Rubin, Helmut Veith, and Josef Widder. 2015. Decidability of Parameterized Verification. Morgan & Claypool Publishers."},{"key":"e_1_2_1_8_1","volume-title":"Foundations of Software Science and Computation Structures, Miko\u0142 aj Boja\u0144czyk and Alex Simpson (Eds.). 11425","author":"Bollig Benedikt","unstructured":"Benedikt Bollig , Patricia Bouyer , and Fabian Reiter . 2019. Identifiers in Registers . In Foundations of Software Science and Computation Structures, Miko\u0142 aj Boja\u0144czyk and Alex Simpson (Eds.). 11425 , Springer International Publishing , Cham . 115\u2013132. isbn:978-3-030-17127-8 Benedikt Bollig, Patricia Bouyer, and Fabian Reiter. 2019. Identifiers in Registers. In Foundations of Software Science and Computation Structures, Miko\u0142 aj Boja\u0144czyk and Alex Simpson (Eds.). 11425, Springer International Publishing, Cham. 115\u2013132. isbn:978-3-030-17127-8"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-10769-6_40"},{"key":"e_1_2_1_10_1","volume-title":"33rd International Conference on Concurrency Theory (CONCUR","author":"Bozga Marius","year":"2022","unstructured":"Marius Bozga , Lucas Bueri , and Radu Iosif . 2022 . On an Invariance Problem for Parameterized Concurrent Systems . In 33rd International Conference on Concurrency Theory (CONCUR 2022), to appear. Marius Bozga, Lucas Bueri, and Radu Iosif. 2022. On an Invariance Problem for Parameterized Concurrent Systems. In 33rd International Conference on Concurrency Theory (CONCUR 2022), to appear."},{"key":"e_1_2_1_11_1","volume-title":"TACAS 2020 (LNCS","volume":"246","author":"Bozga Marius","year":"2020","unstructured":"Marius Bozga , Javier Esparza , Radu Iosif , Joseph Sifakis , and Christoph Welzel . 2020 . Structural Invariants for the Verification of Systems with Parameterized Architectures. In Tools and Algorithms for the Construction and Analysis of Systems - 26th International Conference , TACAS 2020 (LNCS , Vol. 12078). Springer, 228\u2013 246 . Marius Bozga, Javier Esparza, Radu Iosif, Joseph Sifakis, and Christoph Welzel. 2020. Structural Invariants for the Verification of Systems with Parameterized Architectures. In Tools and Algorithms for the Construction and Analysis of Systems - 26th International Conference, TACAS 2020 (LNCS, Vol. 12078). Springer, 228\u2013246."},{"key":"e_1_2_1_12_1","volume-title":"FACS 2021, Virtual Event, October 28-29, 2021, Proceedings (Lecture Notes in Computer Science","volume":"114","author":"Bozga Marius","year":"2021","unstructured":"Marius Bozga and Radu Iosif . 2021 . Specification and Safety Verification of Parametric Hierarchical Distributed Systems. In Formal Aspects of Component Software - 17th International Conference , FACS 2021, Virtual Event, October 28-29, 2021, Proceedings (Lecture Notes in Computer Science , Vol. 13077). Springer, 95\u2013 114 . Marius Bozga and Radu Iosif. 2021. Specification and Safety Verification of Parametric Hierarchical Distributed Systems. In Formal Aspects of Component Software - 17th International Conference, FACS 2021, Virtual Event, October 28-29, 2021, Proceedings (Lecture Notes in Computer Science, Vol. 13077). Springer, 95\u2013114."},{"key":"e_1_2_1_13_1","volume-title":"Verification of Component-based Systems with Recursive Architectures. CoRR, abs\/2112.08292","author":"Bozga Marius","year":"2021","unstructured":"Marius Bozga , Radu Iosif , and Joseph Sifakis . 2021. Verification of Component-based Systems with Recursive Architectures. CoRR, abs\/2112.08292 ( 2021 ), arXiv:2112.08292. arxiv:2112.08292 Marius Bozga, Radu Iosif, and Joseph Sifakis. 2021. Verification of Component-based Systems with Recursive Architectures. CoRR, abs\/2112.08292 (2021), arXiv:2112.08292. arxiv:2112.08292"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1075405.1075411"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2984450.2984457"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exq052"},{"key":"e_1_2_1_17_1","volume-title":"Galeotti","author":"Bucchiarone Antonio","year":"2008","unstructured":"Antonio Bucchiarone and Juan P . Galeotti . 2008 . Dynamic Software Architectures Verification using DynAlloy. Electron. Commun. Eur. Assoc. Softw. Sci. Technol ., 10 (2008). Antonio Bucchiarone and Juan P. Galeotti. 2008. Dynamic Software Architectures Verification using DynAlloy. Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 10 (2008)."},{"key":"e_1_2_1_18_1","volume-title":"Proceedings of MODELS 2017 Satellite Event: Workshops (ModComp) (CEUR Workshop Proceedings","volume":"16","author":"Butting Arvid","year":"2017","unstructured":"Arvid Butting , Robert Heim , Oliver Kautz , Jan Oliver Ringert , Bernhard Rumpe , and Andreas Wortmann . 2017 . A Classification of Dynamic Reconfiguration in Component and Connector Architecture Description . In Proceedings of MODELS 2017 Satellite Event: Workshops (ModComp) (CEUR Workshop Proceedings , Vol. 2019). CEUR-WS.org, 10\u2013 16 . Arvid Butting, Robert Heim, Oliver Kautz, Jan Oliver Ringert, Bernhard Rumpe, and Andreas Wortmann. 2017. A Classification of Dynamic Reconfiguration in Component and Connector Architecture Description. In Proceedings of MODELS 2017 Satellite Event: Workshops (ModComp) (CEUR Workshop Proceedings, Vol. 2019). CEUR-WS.org, 10\u201316."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2049697.2049700"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2007.30"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/0-387-28967-4_2"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/WICSA.2015.21"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/359104.359108"},{"key":"e_1_2_1_24_1","volume-title":"FMCAD","author":"Chen Yu-Fang","year":"2017","unstructured":"Yu-Fang Chen , Chih-Duo Hong , Anthony W. Lin , and Philipp R\u00fcmmer . 2017 . Learning to prove safety over parameterised concurrent systems. In 2017 Formal Methods in Computer Aided Design , FMCAD 2017, Daryl Stewart and Georg Weissenbacher (Eds.). IEEE, 76\u201383. Yu-Fang Chen, Chih-Duo Hong, Anthony W. Lin, and Philipp R\u00fcmmer. 2017. Learning to prove safety over parameterised concurrent systems. In 2017 Formal Methods in Computer Aided Design, FMCAD 2017, Daryl Stewart and Georg Weissenbacher (Eds.). IEEE, 76\u201383."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2013.12.010"},{"key":"e_1_2_1_26_1","first-page":"361","article-title":"A Basic Logic for Reasoning about Connector Reconfiguration","volume":"82","author":"Clarke Dave","year":"2008","unstructured":"Dave Clarke . 2008 . A Basic Logic for Reasoning about Connector Reconfiguration . Fundam. Inf. , 82 , 4 (2008), Feb. , 361 \u2013 390 . issn:0169-2968 Dave Clarke. 2008. A Basic Logic for Reasoning about Connector Reconfiguration. Fundam. Inf., 82, 4 (2008), Feb., 361\u2013390. issn:0169-2968","journal-title":"Fundam. Inf."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3419404"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/503209.503226"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89366-2_26"},{"key":"e_1_2_1_30_1","first-page":"287","article-title":"Views","volume":"48","author":"Dinsdale-Young Thomas","year":"2013","unstructured":"Thomas Dinsdale-Young , Lars Birkedal , Philippa Gardner , Matthew Parkinson , and Hongseok Yang . 2013 . Views : Compositional Reasoning for Concurrent Programs. SIGPLAN Not. , 48 , 1 (2013), Jan. , 287 \u2013 300 . Thomas Dinsdale-Young, Lars Birkedal, Philippa Gardner, Matthew Parkinson, and Hongseok Yang. 2013. Views: Compositional Reasoning for Concurrent Programs. SIGPLAN Not., 48, 1 (2013), Jan., 287\u2013300.","journal-title":"Compositional Reasoning for Concurrent Programs. SIGPLAN Not."},{"key":"e_1_2_1_31_1","volume-title":"Concurrent Abstract Predicates. In ECOOP 2010 \u2013 Object-Oriented Programming. 6183","author":"Dinsdale-Young Thomas","year":"2010","unstructured":"Thomas Dinsdale-Young , Mike Dodds , Philippa Gardner , Matthew J. Parkinson , and Viktor Vafeiadis . 2010 . Concurrent Abstract Predicates. In ECOOP 2010 \u2013 Object-Oriented Programming. 6183 , Springer Berlin Heidelberg, Berlin, Heidelberg. 504\u2013528. Thomas Dinsdale-Young, Mike Dodds, Philippa Gardner, Matthew J. Parkinson, and Viktor Vafeiadis. 2010. Concurrent Abstract Predicates. In ECOOP 2010 \u2013 Object-Oriented Programming. 6183, Springer Berlin Heidelberg, Berlin, Heidelberg. 504\u2013528."},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/0196-6774(82)90023-2"},{"key":"e_1_2_1_33_1","volume-title":"FACS","volume":"217","author":"Dormoy Julien","year":"2010","unstructured":"Julien Dormoy , Olga Kouchnarenko , and Arnaud Lanoix . 2010 . Using Temporal Logic for Dynamic Reconfigurations of Components. In Formal Aspects of Component Software - 7th International Workshop , FACS 2010, Lu\u00eds Soares Barbosa and Markus Lumpe (Eds.) (Lecture Notes in Computer Science , Vol. 6921). Springer, 200\u2013 217 . Julien Dormoy, Olga Kouchnarenko, and Arnaud Lanoix. 2010. Using Temporal Logic for Dynamic Reconfigurations of Components. In Formal Aspects of Component Software - 7th International Workshop, FACS 2010, Lu\u00eds Soares Barbosa and Markus Lumpe (Eds.) (Lecture Notes in Computer Science, Vol. 6921). Springer, 200\u2013217."},{"key":"e_1_2_1_34_1","volume-title":"LPAR 2020: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning","author":"Echenim Mnacho","year":"2020","unstructured":"Mnacho Echenim , Radu Iosif , and Nicolas Peltier . 2020 . Entailment Checking in Separation Logic with Inductive Definitions is 2-EXPTIME hard . In LPAR 2020: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning , Alicante, Spain , May 22-27, 2020 (EPiC Series in Computing, Vol. 73). EasyChair, 191\u2013211. https:\/\/easychair.org\/publications\/paper\/DdNg Mnacho Echenim, Radu Iosif, and Nicolas Peltier. 2020. Entailment Checking in Separation Logic with Inductive Definitions is 2-EXPTIME hard. In LPAR 2020: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Alicante, Spain, May 22-27, 2020 (EPiC Series in Computing, Vol. 73). EasyChair, 191\u2013211. https:\/\/easychair.org\/publications\/paper\/DdNg"},{"key":"e_1_2_1_35_1","doi-asserted-by":"crossref","unstructured":"Rim El-Ballouli Saddek Bensalem Marius Bozga and Joseph Sifakis. 2021. Programming Dynamic Reconfigurable Systems. International Journal on Software Tools for Technology Transfer January. \t\t\t\t  Rim El-Ballouli Saddek Bensalem Marius Bozga and Joseph Sifakis. 2021. Programming Dynamic Reconfigurable Systems. International Journal on Software Tools for Technology Transfer January.","DOI":"10.1007\/s10009-020-00596-7"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3412841.3442017"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434286"},{"key":"e_1_2_1_38_1","volume-title":"Programming Languages and Systems. 4421","author":"Feng Xinyu","unstructured":"Xinyu Feng , Rodrigo Ferreira , and Zhong Shao . 2007. On the Relationship Between Concurrent Separation Logic and Assume-Guarantee Reasoning . In Programming Languages and Systems. 4421 , Springer Berlin Heidelberg , 173\u2013188. Xinyu Feng, Rodrigo Ferreira, and Zhong Shao. 2007. On the Relationship Between Concurrent Separation Logic and Assume-Guarantee Reasoning. In Programming Languages and Systems. 4421, Springer Berlin Heidelberg, 173\u2013188."},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3351452.3351464"},{"key":"e_1_2_1_40_1","volume-title":"What is the Grid? A Three Point Checklist. GRID today, 1","author":"Foster Ian","year":"2002","unstructured":"Ian Foster . 2002. What is the Grid? A Three Point Checklist. GRID today, 1 ( 2002 ), 01, 32\u201336. Ian Foster. 2002. What is the Grid? A Three Point Checklist. GRID today, 1 (2002), 01, 32\u201336."},{"key":"e_1_2_1_41_1","doi-asserted-by":"crossref","unstructured":"Dominik Gall Riko Jacob Andrea Richa Christian Scheideler Stefan Schmid and Hanjo Taeubig. 2014. A Note on the Parallel Runtime of Self-Stabilizing Graph Linearization. Theory of Computing Systems (TOCS). \t\t\t\t  Dominik Gall Riko Jacob Andrea Richa Christian Scheideler Stefan Schmid and Hanjo Taeubig. 2014. A Note on the Parallel Runtime of Self-Stabilizing Graph Linearization. Theory of Computing Systems (TOCS).","DOI":"10.1007\/s00224-013-9504-x"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-23702-7_7"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/288408.288426"},{"key":"#cr-split#-e_1_2_1_44_1.1","unstructured":"Radu Iosif and Florian Zuleger. 2022. On the Expressiveness of a Logic of Separated Relations. https:\/\/doi.org\/10.48550\/ARXIV.2208.01520 10.48550\/ARXIV.2208.01520"},{"key":"#cr-split#-e_1_2_1_44_1.2","unstructured":"Radu Iosif and Florian Zuleger. 2022. On the Expressiveness of a Logic of Separated Relations. https:\/\/doi.org\/10.48550\/ARXIV.2208.01520"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/505145.505149"},{"key":"e_1_2_1_47_1","volume-title":"Beyond Symbolic Heaps: Deciding Separation Logic With Inductive Definitions. In LPAR 2020: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning","author":"Katelaan Jens","year":"2020","unstructured":"Jens Katelaan and Florian Zuleger . 2020 . Beyond Symbolic Heaps: Deciding Separation Logic With Inductive Definitions. In LPAR 2020: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning , Alicante, Spain , May 22-27, 2020 (EPiC Series in Computing, Vol. 73). EasyChair, 390\u2013408. https:\/\/easychair.org\/publications\/paper\/VTGk Jens Katelaan and Florian Zuleger. 2020. Beyond Symbolic Heaps: Deciding Separation Logic With Inductive Definitions. In LPAR 2020: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Alicante, Spain, May 22-27, 2020 (EPiC Series in Computing, Vol. 73). EasyChair, 390\u2013408. https:\/\/easychair.org\/publications\/paper\/VTGk"},{"key":"e_1_2_1_48_1","volume-title":"Parameterized Systems in BIP: Design and Model Checking. In 27th International Conference on Concurrency Theory, CONCUR 2016 (LIPIcs","volume":"16","author":"Konnov Igor V.","year":"2016","unstructured":"Igor V. Konnov , Tomer Kotek , Qiang Wang , Helmut Veith , Simon Bliudze , and Joseph Sifakis . 2016 . Parameterized Systems in BIP: Design and Model Checking. In 27th International Conference on Concurrency Theory, CONCUR 2016 (LIPIcs , Vol. 59). Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 30:1\u201330: 16 . Igor V. Konnov, Tomer Kotek, Qiang Wang, Helmut Veith, Simon Bliudze, and Joseph Sifakis. 2016. Parameterized Systems in BIP: Design and Model Checking. In 27th International Conference on Concurrency Theory, CONCUR 2016 (LIPIcs, Vol. 59). Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 30:1\u201330:16."},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2009.10.006"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9939-1956-0078686-7"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/279227.279229"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/357172.357176"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2011.11.011"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.708567"},{"key":"e_1_2_1_55_1","first-page":"219","article-title":"An introduction to input\/output automata","volume":"2","author":"Lynch Nancy","year":"1989","unstructured":"Nancy Lynch and M.R. Tuttle . 1989 . An introduction to input\/output automata . CWI Quarterly , 2 , 3 (1989), Sept. , 219 \u2013 246 . Nancy Lynch and M.R. Tuttle. 1989. An introduction to input\/output automata. CWI Quarterly, 2, 3 (1989), Sept., 219\u2013246.","journal-title":"CWI Quarterly"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/250707.239104"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2016.05.002"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/3382734.3405744"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1109\/COMST.2017.2782753"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.035"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.5555\/647851.737404"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/1498926.1498929"},{"key":"e_1_2_1_63_1","volume-title":"An Axiomatic Proof Technique for Parallel Programs","author":"Owicki Susan","unstructured":"Susan Owicki and David Gries . 1978. An Axiomatic Proof Technique for Parallel Programs . Springer New York, New York , NY. 130\u2013152. Susan Owicki and David Gries. 1978. An Axiomatic Proof Technique for Parallel Programs. Springer New York, New York, NY. 130\u2013152."},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1109\/INFOCOM.2019.8737417"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1002\/j.1538-7305.1957.tb01515.x"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1109\/TNET.2015.2410313"},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/3022671.2983999"},{"key":"e_1_2_1_69_1","volume-title":"International Workshop, Joseph Sifakis (Ed.) (LNCS","volume":"165","author":"Shtadler Ze\u2019ev","year":"1989","unstructured":"Ze\u2019ev Shtadler and Orna Grumberg . 1989 . Network Grammars, Communication Behaviors and Automatic Verification. In Automatic Verification Methods for Finite State Systems , International Workshop, Joseph Sifakis (Ed.) (LNCS , Vol. 407). Springer, 151\u2013 165 . Ze\u2019ev Shtadler and Orna Grumberg. 1989. Network Grammars, Communication Behaviors and Automatic Verification. In Automatic Verification Methods for Finite State Systems, International Workshop, Joseph Sifakis (Ed.) (LNCS, Vol. 407). Springer, 151\u2013165."},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/3828.3835"},{"key":"e_1_2_1_71_1","volume-title":"International Workshop on Theory and Application of Graph Transformations. 179\u2013193","author":"Taentzer Gabriele","year":"1998","unstructured":"Gabriele Taentzer , Michael Goedicke , and Torsten Meyer . 1998 . Dynamic change management by distributed graph transformation: Towards configurable distributed systems . In International Workshop on Theory and Application of Graph Transformations. 179\u2013193 . Gabriele Taentzer, Michael Goedicke, and Torsten Meyer. 1998. Dynamic change management by distributed graph transformation: Towards configurable distributed systems. In International Workshop on Theory and Application of Graph Transformations. 179\u2013193."},{"key":"e_1_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74407-8_18"},{"key":"e_1_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1049\/ip-sen:19982294"},{"key":"e_1_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(02)00036-9"},{"key":"e_1_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1145\/503271.503213"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3563293","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3563293","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:38:10Z","timestamp":1750178290000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3563293"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,10,31]]},"references-count":74,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2022,10,31]]}},"alternative-id":["10.1145\/3563293"],"URL":"https:\/\/doi.org\/10.1145\/3563293","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,10,31]]},"assertion":[{"value":"2022-10-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}