{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,16]],"date-time":"2026-10-16T21:12:28Z","timestamp":1792185148326,"version":"4.4.0"},"reference-count":106,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2022,3,7]],"date-time":"2022-03-07T00:00:00Z","timestamp":1646611200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100003407","name":"MIUR","doi-asserted-by":"crossref","award":["PRIN 2017FTXR7S"],"award-info":[{"award-number":["PRIN 2017FTXR7S"]}],"id":[{"id":"10.13039\/501100003407","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Softw. Eng. Methodol."],"published-print":{"date-parts":[[2022,7,31]]},"abstract":"<jats:p>Sequential emulation is a semantics-based technique to automatically reduce property checking of distributed systems to the analysis of sequential programs. An automated procedure takes as input a formal specification of a distributed system, a property of interest, and the structural operational semantics of the specification language and generates a sequential program whose execution traces emulate the possible evolutions of the considered system. The problem as to whether the property of interest holds for the system can then be expressed either as a reachability or as a termination query on the program. This allows to immediately adapt mature verification techniques developed for general-purpose languages to domain-specific languages, and to effortlessly integrate new techniques as soon as they become available. We test our approach on a selection of concurrent systems originated from different contexts from population protocols to models of flocking behaviour. By combining a comprehensive range of program verification techniques, from traditional symbolic execution to modern inductive-based methods such as property-directed reachability, we are able to draw consistent and correct verification verdicts for the considered systems.<\/jats:p>","DOI":"10.1145\/3490387","type":"journal-article","created":{"date-parts":[[2022,3,7]],"date-time":"2022-03-07T10:24:54Z","timestamp":1646648694000},"page":"1-41","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":12,"title":["Verification of Distributed Systems via Sequential Emulation"],"prefix":"10.1145","volume":"31","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1922-3151","authenticated-orcid":false,"given":"Luca","family":"Di Stefano","sequence":"first","affiliation":[{"name":"University Grenoble Alpes, Inria, CNRS, Grenoble INP, LIG, Inria, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4691-7570","authenticated-orcid":false,"given":"Rocco","family":"De Nicola","sequence":"additional","affiliation":[{"name":"IMT School of Advanced Studies, Lucca, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9348-1979","authenticated-orcid":false,"given":"Omar","family":"Inverso","sequence":"additional","affiliation":[{"name":"Gran Sasso Science Institute (GSSI), L\u2019Aquila, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,3,7]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2020.102428"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00446-008-0059-z"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-89707-1_5"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/3133934"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1073\/pnas.0711437105"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49674-9_55"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17502-3_9"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-007-0044-z"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_16"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37057-1_11"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49059-0_14"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96145-3_34"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.5555\/554879"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2008.17"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96142-2_23"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10431-7_20"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54580-5_28"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2015.10"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_24"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/876638.876643"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32759-9_14"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/2790449.2790529"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-09766-4_450"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2019.102345"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-61470-6_16"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-67531-2_11"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.5348289"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-50029-0_23"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-34327-8_20"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.5555\/2157654.2157675"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2013.6693139"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.5555\/556746"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.07.004"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.1145\/3238147.3240481"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19835-9_33"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-68270-9_1"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-016-9388-y"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-63166-6_10"},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-08755-9_9"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","DOI":"10.1126\/science.1116681"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSC.2015.2413401"},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49674-9_69"},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_20"},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","DOI":"10.1109\/SocialCom.2010.107"},{"key":"e_1_3_2_48_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_2"},{"key":"e_1_3_2_49_2","first-page":"235","volume-title":"Proceedings of the IJCAI","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 IJCAI. William Kaufmann, 235\u2013245."},{"key":"e_1_3_2_50_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.cogsys.2015.12.002"},{"key":"e_1_3_2_51_2","doi-asserted-by":"publisher","DOI":"10.5555\/3921"},{"key":"e_1_3_2_52_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0269888918000176"},{"key":"e_1_3_2_53_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_39"},{"key":"e_1_3_2_54_2","doi-asserted-by":"publisher","DOI":"10.1145\/3332466.3374529"},{"key":"e_1_3_2_55_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSC.2015.2449850"},{"key":"e_1_3_2_56_2","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"e_1_3_2_57_2","doi-asserted-by":"publisher","DOI":"10.1109\/IROS.2004.1389727"},{"key":"e_1_3_2_58_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_2"},{"key":"e_1_3_2_59_2","doi-asserted-by":"publisher","DOI":"10.1145\/3360549"},{"key":"e_1_3_2_60_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2016.03.006"},{"key":"e_1_3_2_61_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15461-4_42"},{"key":"e_1_3_2_62_2","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v29i1.9442"},{"key":"e_1_3_2_63_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-34327-8_34"},{"key":"e_1_3_2_64_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_7"},{"key":"e_1_3_2_65_2","volume-title":"Specifying Systems, the TLA+ Language and Tools for Hardware and Software Engineers","author":"Lamport Leslie","year":"2002","unstructured":"Leslie Lamport. 2002. Specifying Systems, the TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley."},{"key":"e_1_3_2_66_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-30942-8_13"},{"key":"e_1_3_2_67_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-16612-9_11"},{"key":"e_1_3_2_68_2","doi-asserted-by":"publisher","DOI":"10.24963\/ijcai.2018\/56"},{"key":"e_1_3_2_69_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-015-0378-x"},{"key":"e_1_3_2_70_2","doi-asserted-by":"publisher","DOI":"10.1177\/0037549705058073"},{"key":"e_1_3_2_71_2","first-page":"432","volume-title":"Proceedings of the 2nd International Conference on Adaptive Behavior from Animals to Animats 2","author":"Matari\u0107 Maja J.","year":"1993","unstructured":"Maja J. Matari\u0107. 1993. Designing emergent behaviors: From local interactions to collective intelligence. In Proceedings of the 2nd International Conference on Adaptive Behavior from Animals to Animats 2. MIT Press, 432\u2013441."},{"key":"e_1_3_2_72_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)71948-7"},{"key":"e_1_3_2_73_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-10235-3"},{"key":"e_1_3_2_74_2","volume-title":"Communication and Concurrency","author":"Milner Robin","year":"1989","unstructured":"Robin Milner. 1989. Communication and Concurrency. Prentice Hall."},{"key":"e_1_3_2_75_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2004.03.008"},{"key":"e_1_3_2_76_2","volume-title":"A Compositional Interchange Format for Hybrid Systems: Design and Implementation","author":"Agut D. E Nadales","year":"2012","unstructured":"D. E Nadales Agut. 2012. A Compositional Interchange Format for Hybrid Systems: Design and Implementation. PhD Thesis. Technische Universiteit Eindhoven."},{"key":"e_1_3_2_77_2","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2005.864190"},{"key":"e_1_3_2_78_2","volume-title":"Business Process Model And Notation - Version 2.0","year":"2010","unstructured":"OMG. 2010. Business Process Model And Notation - Version 2.0. Technical Report dtc\/2010-05-03."},{"key":"e_1_3_2_79_2","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908118"},{"key":"e_1_3_2_80_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1018980001403"},{"key":"e_1_3_2_81_2","doi-asserted-by":"publisher","DOI":"10.7561\/SACS.2013.1.119"},{"key":"e_1_3_2_82_2","first-page":"287","volume-title":"Proceedings of the 9th EAI International Conference on Bio-Inspired Information and Communications Technologies","author":"Pinciroli Carlo","year":"2015","unstructured":"Carlo Pinciroli, Adam Lee-Brown, and Giovanni Beltrame. 2015. A tuple space for data sharing in robot swarms. In Proceedings of the 9th EAI International Conference on Bio-Inspired Information and Communications Technologies. ICST\/ACM, 287\u2013294."},{"key":"e_1_3_2_83_2","doi-asserted-by":"publisher","DOI":"10.1007\/S11721-012-0072-5"},{"key":"e_1_3_2_84_2","volume-title":"A Structural Approach to Operational Semantics","author":"Plotkin Gordon D.","year":"1981","unstructured":"Gordon D. Plotkin. 1981. A Structural Approach to Operational Semantics. Technical Report DAIMI FN-19. Computer Science Department, Aarhus University. Reprinted in J. Log. Algebr. Program., 2004."},{"key":"e_1_3_2_85_2","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_3_2_86_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31980-1_7"},{"key":"e_1_3_2_87_2","doi-asserted-by":"publisher","DOI":"10.1145\/1242572.1242704"},{"key":"e_1_3_2_88_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_7"},{"key":"e_1_3_2_89_2","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199462"},{"key":"e_1_3_2_90_2","doi-asserted-by":"publisher","DOI":"10.1145\/37402.37406"},{"key":"e_1_3_2_91_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-90686-7_13"},{"key":"e_1_3_2_92_2","doi-asserted-by":"publisher","DOI":"10.1109\/IROS.2013.6696520"},{"issue":"1","key":"e_1_3_2_93_2","first-page":"39","article-title":"Realizability and dynamic reconfiguration of chor specifications","volume":"35","author":"Roohi Nima","year":"2011","unstructured":"Nima Roohi and Gwen Sala\u00fcn. 2011. Realizability and dynamic reconfiguration of chor specifications. Informatica 35, 1 (2011), 39\u201349.","journal-title":"Informatica"},{"key":"e_1_3_2_94_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49674-9_56"},{"key":"e_1_3_2_95_2","doi-asserted-by":"publisher","DOI":"10.1145\/3158116"},{"key":"e_1_3_2_96_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-40922-X_8"},{"key":"e_1_3_2_97_2","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2984027"},{"key":"e_1_3_2_98_2","doi-asserted-by":"publisher","DOI":"10.1006\/bulm.2001.0252"},{"key":"e_1_3_2_99_2","doi-asserted-by":"publisher","DOI":"10.1137\/S009753979628292X"},{"key":"e_1_3_2_100_2","doi-asserted-by":"publisher","DOI":"10.1162\/106454602753694765"},{"key":"e_1_3_2_101_2","doi-asserted-by":"publisher","DOI":"10.1162\/106454699568700"},{"key":"e_1_3_2_102_2","doi-asserted-by":"publisher","DOI":"10.1109\/MITP.2012.18"},{"key":"e_1_3_2_103_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2015.01.007"},{"key":"e_1_3_2_104_2","volume-title":"Web Services Choreography Description Language - Version 1.0","year":"2005","unstructured":"W3C. 2005. Web Services Choreography Description Language - Version 1.0. Technical Report."},{"key":"e_1_3_2_105_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4419-6984-2_12"},{"key":"e_1_3_2_106_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(84)90112-9"},{"key":"e_1_3_2_107_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48153-2_6"}],"container-title":["ACM Transactions on Software Engineering and Methodology"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3490387","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3490387","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:30:43Z","timestamp":1750188643000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3490387"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,3,7]]},"references-count":106,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2022,7,31]]}},"alternative-id":["10.1145\/3490387"],"URL":"https:\/\/doi.org\/10.1145\/3490387","relation":{},"ISSN":["1049-331X","1557-7392"],"issn-type":[{"value":"1049-331X","type":"print"},{"value":"1557-7392","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,3,7]]},"assertion":[{"value":"2021-01-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-10-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-03-07","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}