{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,8]],"date-time":"2026-07-08T22:31:05Z","timestamp":1783549865516,"version":"3.55.0"},"publisher-location":"Cham","reference-count":39,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030451899","type":"print"},{"value":"9783030451905","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-45190-5_13","type":"book-chapter","created":{"date-parts":[[2020,4,17]],"date-time":"2020-04-17T09:03:02Z","timestamp":1587114182000},"page":"228-246","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Structural Invariants for the Verification of Systems with Parameterized Architectures"],"prefix":"10.1007","author":[{"given":"Marius","family":"Bozga","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9862-4919","authenticated-orcid":false,"given":"Javier","family":"Esparza","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Radu","family":"Iosif","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Joseph","family":"Sifakis","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5583-0640","authenticated-orcid":false,"given":"Christoph","family":"Welzel","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2020,4,17]]},"reference":[{"key":"13_CR1","unstructured":"Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.: General decidability theorems for infinite-state systems. In: LICS. pp. 313\u2013321. IEEE Computer Society (1996)"},{"key":"13_CR2","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Delzanno, G., Henda, N.B., Rezine, A.: Regular model checking without transducers (on efficient verification of parameterized systems). In: Grumberg, O., Huth, M. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. pp. 721\u2013736 (2007)","DOI":"10.1007\/978-3-540-71209-1_56"},{"key":"13_CR3","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Haziza, F., Hol\u00edk, L.: Parameterized verification through view abstraction. STTT 18(5), 495\u2013516 (2016)","DOI":"10.1007\/s10009-015-0406-x"},{"key":"13_CR4","unstructured":"Alberti, F., Ghilardi, S., Sharygina, N.: A framework for the verification of parameterized infinite-state systems. CEUR Workshop Proceedings 1195, 302\u2013308 (01 2014)"},{"key":"13_CR5","doi-asserted-by":"crossref","unstructured":"Aminof, B., Kotek, T., Rubin, S., Spegni, F., Veith, H.: Parameterized model checking of rendezvous systems. Distributed Computing 31(3), 187\u2013222 (Jun 2018)","DOI":"10.1007\/s00446-017-0302-6"},{"key":"13_CR6","doi-asserted-by":"crossref","unstructured":"Apt, K.R., Kozen, D.C.: Limits for automatic verification of finite-state concurrent systems. Information Processing Letters 22(6), 307 \u2013 309 (1986)","DOI":"10.1016\/0020-0190(86)90071-2"},{"key":"13_CR7","doi-asserted-by":"crossref","unstructured":"Au\u00dferlechner, S., Jacobs, S., Khalimov, A.: Tight cutoffs for guarded protocols with fairness. In: VMCAI. Lecture Notes in Computer Science, vol. 9583, pp. 476\u2013494. Springer (2016)","DOI":"10.1007\/978-3-662-49122-5_23"},{"key":"13_CR8","unstructured":"Barkaoui, K., Lemaire, B.: An effective characterization of minimal deadlocks and traps in Petri nets based on graph theory. In: 10th Int. Conf. on Application and Theory of Petri Nets ICATPN\u201989. pp. 1\u201321 (1989)"},{"key":"13_CR9","doi-asserted-by":"crossref","unstructured":"Basu, A., Bensalem, S., Bozga, M., Combaz, J., Jaber, M., Nguyen, T., Sifakis, J.: Rigorous component-based system design using the BIP framework. IEEE Software 28(3), 41\u201348 (2011)","DOI":"10.1109\/MS.2011.27"},{"key":"13_CR10","doi-asserted-by":"crossref","unstructured":"Baukus, K., Bensalem, S., Lakhnech, Y., Stahl, K.: Abstracting WS1S systems to verify parameterized networks. In: Graf, S., Schwartzbach, M. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. pp. 188\u2013203 (2000)","DOI":"10.1007\/3-540-46419-0_14"},{"key":"13_CR11","doi-asserted-by":"crossref","unstructured":"Bensalem, S., Bozga, M., Nguyen, T., Sifakis, J.: D-Finder: A tool for compositional deadlock detection and verification. In: CAV\u201909 Proceedings. LNCS, vol. 5643, pp. 614\u2013619 (2009)","DOI":"10.1007\/978-3-642-02658-4_45"},{"key":"13_CR12","doi-asserted-by":"crossref","unstructured":"Bloem, R., Jacobs, S., Khalimov, A., Konnov, I., Rubin, S., Veith, H., Widder, J.: Decidability of Parameterized Verification. Synthesis Lectures on Distributed Computing Theory, Morgan & Claypool Publishers (2015)","DOI":"10.2200\/S00658ED1V01Y201508DCT013"},{"key":"13_CR13","doi-asserted-by":"crossref","unstructured":"Blondin, M., Finkel, A., Haase, C., Haddad, S.: Approaching the coverability problem continuously. In: TACAS. Lecture Notes in Computer Science, vol. 9636, pp. 480\u2013496. Springer (2016)","DOI":"10.1007\/978-3-662-49674-9_28"},{"key":"13_CR14","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Habermehl, P., Vojnar, T.: Abstract regular model checking. In: Alur, R., Peled, D.A. (eds.) Computer Aided Verification. pp. 372\u2013386 (2004)","DOI":"10.1007\/978-3-540-27813-9_29"},{"key":"13_CR15","unstructured":"Bozga, M., Esparza, J., Iosif, R., Sifakis, J., Welzel, C.: ostrich (Feb 2020), \nhttps:\/\/doi.org\/10.5281\/zenodo.3676940"},{"key":"13_CR16","doi-asserted-by":"crossref","unstructured":"Bozga, M., Esparza, J., Iosif, R., Sifakis, J., Welzel, C.: Structural invariants for the verification of systems with parameterized architectures (2020)","DOI":"10.1007\/978-3-030-45190-5_13"},{"key":"13_CR17","doi-asserted-by":"crossref","unstructured":"Bozga, M., Iosif, R., Sifakis, J.: Checking deadlock-freedom of parametric component-based systems. In: 25th Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). (2019)","DOI":"10.1007\/978-3-030-17465-1_1"},{"key":"13_CR18","doi-asserted-by":"crossref","unstructured":"Browne, M., Clarke, E., Grumberg, O.: Reasoning about networks with many identical finite state processes. Information and Computation 81(1), 13 \u2013 31 (1989)","DOI":"10.1016\/0890-5401(89)90026-6"},{"key":"13_CR19","unstructured":"Chen, Y., Hong, C., Lin, A.W., R\u00fcmmer, P.: Learning to prove safety over parameterised concurrent systems. In: 2017 Formal Methods in Computer Aided Design, FMCAD 2017, Vienna, Austria, October 2-6, 2017. pp. 76\u201383 (2017)"},{"key":"13_CR20","doi-asserted-by":"crossref","unstructured":"Clarke, E., Talupur, M., Veith, H.: Environment abstraction for parameterized verification. In: Emerson, E.A., Namjoshi, K.S. (eds.) Verification, Model Checking, and Abstract Interpretation. pp. 126\u2013141 (2006)","DOI":"10.1007\/11609773_9"},{"key":"13_CR21","doi-asserted-by":"crossref","unstructured":"Conchon, S., Goel, A., Krsti\u0107, S., Mebsout, A., Za\u00efdi, F.: Cubicle: A parallel SMT-based model checker for parameterized systems. In: Madhusudan, P., Seshia, S.A. (eds.) Computer Aided Verification. pp. 718\u2013724 (2012)","DOI":"10.1007\/978-3-642-31424-7_55"},{"key":"13_CR22","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Conference Record of the Sixth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. pp. 269\u2013282. ACM Press, New York, NY, San Antonio, Texas (1979)","DOI":"10.1145\/567752.567778"},{"key":"13_CR23","doi-asserted-by":"crossref","unstructured":"Dams, D., Lakhnech, Y., Steffen, M.: Iterating transducers. The Journal of Logic and Algebraic Programming 52-53, 109 \u2013 127 (2002)","DOI":"10.1016\/S1567-8326(02)00025-5"},{"key":"13_CR24","doi-asserted-by":"crossref","unstructured":"Delzanno, G.: Automatic verification of parameterized cache coherence protocols. In: Computer Aided Verification, 12th International Conference, CAV 2000, Chicago, IL, USA, July 15-19, 2000, Proceedings. pp. 53\u201368 (2000)","DOI":"10.1007\/10722167_8"},{"key":"13_CR25","unstructured":"Dijkstra, E.W., Scholten, C.S.: Termination detection for diffusing computations. Inf. Process. Lett. 11(1), 1\u20134 (1980)"},{"key":"13_CR26","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Kahlon, V.: Reducing model checking of the many to the few. In: CADE. Lecture Notes in Computer Science, vol. 1831, pp. 236\u2013254. Springer (2000)","DOI":"10.1007\/10721959_19"},{"key":"13_CR27","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Namjoshi, K.S.: Reasoning about rings. In: POPL\u201995 Proceedings. pp. 85\u201394 (1995).","DOI":"10.1145\/199448.199468"},{"key":"13_CR28","doi-asserted-by":"crossref","unstructured":"Esparza, J., Ledesma-Garza, R., Majumdar, R., Meyer, P.J., Niksic, F.: An smt-based approach to coverability analysis. In: CAV. Lecture Notes in Computer Science, vol. 8559, pp. 603\u2013619. Springer (2014)","DOI":"10.1007\/978-3-319-08867-9_40"},{"key":"13_CR29","doi-asserted-by":"crossref","unstructured":"Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere! Theor. Comput. Sci. 256(1-2), 63\u201392 (2001)","DOI":"10.1016\/S0304-3975(00)00102-X"},{"key":"13_CR30","doi-asserted-by":"crossref","unstructured":"Fribourg, L., Ols\u00e9n, H.: Reachability sets of parameterized rings as regular languages. Electr. Notes Theor. Comput. Sci. 9, \u00a040 (1997)","DOI":"10.1016\/S1571-0661(05)80427-X"},{"key":"13_CR31","doi-asserted-by":"crossref","unstructured":"German, S.M., Sistla, A.P.: Reasoning about systems with many processes. J. ACM 39(3), 675\u2013735 (1992)","DOI":"10.1145\/146637.146681"},{"key":"13_CR32","unstructured":"Hartmanns, A., Seidl, M.: tacas20ae.ova (10 2019), \nhttps:\/\/figshare.com\/articles\/tacas20ae_ova\/9699839"},{"key":"13_CR33","doi-asserted-by":"crossref","unstructured":"Henriksen, J., Jensen, J., J\u00f8rgensen, M., Klarlund, N., Paige, B., Rauhe, T., Sandholm, A.: Mona: Monadic second-order logic in practice. In: Tools and Algorithms for the Construction and Analysis of Systems, First International Workshop, TACAS \u201995, LNCS 1019 (1995)","DOI":"10.7146\/brics.v2i21.19923"},{"key":"13_CR34","doi-asserted-by":"crossref","unstructured":"Jacobs, S., Sakr, M.: Analyzing guarded protocols: Better cutoffs, more systems, more expressivity. In: VMCAI. Lecture Notes in Computer Science, vol. 10747, pp. 247\u2013268. Springer (2018)","DOI":"10.1007\/978-3-319-73721-8_12"},{"key":"13_CR35","doi-asserted-by":"crossref","unstructured":"Jensen, H.E., Lynch, N.A.: A proof of Burns n-process mutual exclusion algorithm using abstraction. In: TACAS (1998)","DOI":"10.1007\/BFb0054186"},{"key":"13_CR36","doi-asserted-by":"crossref","unstructured":"Kesten, Y., Maler, O., Marcus, M., Pnueli, A., Shahar, E.: Symbolic model checking with rich assertional languages. Theoretical Computer Science 256(1), 93 \u2013 112 (2001)","DOI":"10.1016\/S0304-3975(00)00103-1"},{"key":"13_CR37","doi-asserted-by":"crossref","unstructured":"Khoussainov, B., Nerode, A.: Automata Theory and Its Applications. Birkhauser Boston, Inc. (2001).","DOI":"10.1007\/978-1-4612-0171-7"},{"key":"13_CR38","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Ruah, S., Zuck, L.: Automatic deductive verification with invisible invariants. In: Margaria, T., Yi, W. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. pp. 82\u201397 (2001)","DOI":"10.1007\/3-540-45319-9_7"},{"key":"13_CR39","doi-asserted-by":"crossref","unstructured":"Sifakis, J.: Structural properties of petri nets. In: Winkowski, J. (ed.) Mathematical Foundations of Computer Science 1978. pp. 474\u2013483 (1978)","DOI":"10.1007\/3-540-08921-7_95"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-45190-5_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,8,20]],"date-time":"2020-08-20T13:10:57Z","timestamp":1597929057000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-45190-5_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030451899","9783030451905"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-45190-5_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"17 April 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Dublin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Ireland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 April 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 April 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/2020\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Easychair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"155","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"40","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"8","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"26% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"14","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference could not take place due to the COVID-19 pandemic. There was an online event on July 2, 2020.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}