{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T22:28:13Z","timestamp":1784845693048,"version":"3.55.0"},"reference-count":43,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2016,6,3]],"date-time":"2016-06-03T00:00:00Z","timestamp":1464912000000},"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":["SIGACT News"],"published-print":{"date-parts":[[2016,6,3]]},"DOI":"10.1145\/2951860.2951873","type":"journal-article","created":{"date-parts":[[2016,6,10]],"date-time":"2016-06-10T13:00:33Z","timestamp":1465563633000},"page":"53-64","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":25,"title":["Decidability in Parameterized Verification"],"prefix":"10.1145","volume":"47","author":[{"given":"Roderick","family":"Bloem","sequence":"first","affiliation":[{"name":"TU Graz, Graz, Austria"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Swen","family":"Jacobs","sequence":"additional","affiliation":[{"name":"Universit\u00e4t des Saarlandes, Saarbr\u00fccken, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ayrat","family":"Khalimov","sequence":"additional","affiliation":[{"name":"TU Graz,Graz, Austria"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Igor","family":"Konnov","sequence":"additional","affiliation":[{"name":"TU Wien, Vienna, Austria"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sasha","family":"Rubin","sequence":"additional","affiliation":[{"name":"Universit\u00e0 degli Studi di Napoli \"Federico II\", Naples, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Helmut","family":"Veith","sequence":"additional","affiliation":[{"name":"TU Wien, Vienna, Austria"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Josef","family":"Widder","sequence":"additional","affiliation":[{"name":"TU Wien, Vienna, Austria"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2016,6,3]]},"reference":[{"key":"e_1_2_1_1_1","series-title":"LNCS","first-page":"193","volume-title":"FORTE","author":"Abdulla P. A.","year":"2013","unstructured":"P. A. Abdulla , M. F. Atig , and O. Rezine . Verification of directed acyclic ad hoc networks . In FORTE , volume 7892 of LNCS , pages 193 -- 208 . Springer , 2013 . P. A. Abdulla, M. F. Atig, and O. Rezine. Verification of directed acyclic ad hoc networks. In FORTE, volume 7892 of LNCS, pages 193--208. Springer, 2013."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/788018.788796"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-008-0062-9"},{"key":"e_1_2_1_4_1","series-title":"LNCS","first-page":"35","volume-title":"CONCUR","author":"Abdulla P. A.","year":"2004","unstructured":"P. A. Abdulla , B. Jonsson , M. Nilsson , and M. Saksena . A survey of regular model checking . In CONCUR , volume 3170 of LNCS , pages 35 -- 48 . Springer , 2004 . P. A. Abdulla, B. Jonsson, M. Nilsson, and M. Saksena. A survey of regular model checking. In CONCUR, volume 3170 of LNCS, pages 35--48. Springer, 2004."},{"key":"e_1_2_1_5_1","series-title":"LNCS","first-page":"262","volume-title":"VMCAI","author":"Aminof B.","year":"2014","unstructured":"B. Aminof , S. Jacobs , A. Khalimov , and S. Rubin . Parameterized model checking of tokenpassing systems . In VMCAI , volume 8318 of LNCS , pages 262 -- 281 , Jan. 2014 . B. Aminof, S. Jacobs, A. Khalimov, and S. Rubin. Parameterized model checking of tokenpassing systems. In VMCAI, volume 8318 of LNCS, pages 262--281, Jan. 2014."},{"key":"e_1_2_1_6_1","first-page":"109","volume":"8704","author":"Aminof B.","year":"2014","unstructured":"B. Aminof , T. Kotek , S. Rubin , F. Spegni , and H. Veith . Parameterized model checking of rendezvous systems. In CONCUR , volume 8704 , pages 109 -- 124 . Springer, 2014 . B. Aminof, T. Kotek, S. Rubin, F. Spegni, and H. Veith. Parameterized model checking of rendezvous systems. In CONCUR, volume 8704, pages 109--124. Springer, 2014.","journal-title":"Parameterized model checking of rendezvous systems. In CONCUR"},{"key":"e_1_2_1_7_1","volume-title":"Logic for Programming, Artificial Intelligence","author":"Aminof B.","year":"2015","unstructured":"B. Aminof , S. Rubin , and F. Zuleger . On the expressive power of communication primitives in parameterised systems . In M. Davis, A. Voronkov, A. McIver, and A. Fehnker, editors, Logic for Programming, Artificial Intelligence , and Reasoning , 2015 . B. Aminof, S. Rubin, and F. Zuleger. On the expressive power of communication primitives in parameterised systems. In M. Davis, A. Voronkov, A. McIver, and A. Fehnker, editors, Logic for Programming, Artificial Intelligence, and Reasoning, 2015."},{"key":"e_1_2_1_8_1","doi-asserted-by":"crossref","DOI":"10.1002\/0471478210","volume-title":"Distributed Computing","author":"Attiya H.","year":"2004","unstructured":"H. Attiya and J. Welch . Distributed Computing . John Wiley & Sons , 2 nd edition, 2004 . H. Attiya and J. Welch. Distributed Computing. John Wiley & Sons, 2nd edition, 2004.","edition":"2"},{"key":"e_1_2_1_9_1","volume-title":"FAST: acceleration from theory to practice. STTT, 10(5):401--424","author":"Bardin S.","year":"2008","unstructured":"S. Bardin , A. Finkel , J. Leroux , and L. Petrucci . FAST: acceleration from theory to practice. STTT, 10(5):401--424 , 2008 . S. Bardin, A. Finkel, J. Leroux, and L. Petrucci. FAST: acceleration from theory to practice. STTT, 10(5):401--424, 2008."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_9"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/2886151"},{"key":"e_1_2_1_12_1","volume-title":"ByMC: Byzantine model checker","author":"MC.","year":"2013","unstructured":"By MC. ByMC: Byzantine model checker , 2013 . URL : http:\/\/forsyte.tuwien.ac.at\/software\/bymc\/. Accessed : April, 2016. ByMC. ByMC: Byzantine model checker, 2013. URL: http:\/\/forsyte.tuwien.ac.at\/software\/bymc\/. Accessed: April, 2016."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_22"},{"key":"e_1_2_1_14_1","volume-title":"Model Checking","author":"Clarke E.","year":"1999","unstructured":"E. Clarke , O. Grumberg , and D. Peled . Model Checking . MIT Press , 1999 . E. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-28644-8_18"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_55"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-016-0412-7"},{"key":"e_1_2_1_18_1","series-title":"LNCS","first-page":"173","volume-title":"TACAS","author":"Delzanno G.","year":"2002","unstructured":"G. Delzanno , J. Raskin , and L. Van Begin . Towards the automated verification of multithreaded Java programs . In TACAS , volume 2280 of LNCS , pages 173 -- 187 , 2002 . G. Delzanno, J. Raskin, and L. Van Begin. Towards the automated verification of multithreaded Java programs. In TACAS, volume 2280 of LNCS, pages 173--187, 2002."},{"key":"e_1_2_1_19_1","first-page":"313","volume":"6269","author":"Delzanno G.","year":"2010","unstructured":"G. Delzanno , A. Sangnier , and G. Zavattaro . Parameterized verification of ad hoc networks. In CONCUR , volume 6269 of LNCS, pages 313 -- 327 , 2010 . G. Delzanno, A. Sangnier, and G. Zavattaro. Parameterized verification of ad hoc networks. In CONCUR, volume 6269 of LNCS, pages 313--327, 2010.","journal-title":"Parameterized verification of ad hoc networks. In CONCUR"},{"key":"e_1_2_1_20_1","series-title":"LNCS","first-page":"441","volume-title":"FOSSACS","author":"Delzanno G.","year":"2011","unstructured":"G. Delzanno , A. Sangnier , and G. Zavattaro . On the power of cliques in the parameterized verification of ad hoc networks . In FOSSACS , volume 6604 of LNCS , pages 441 -- 455 . Springer , 2011 . G. Delzanno, A. Sangnier, and G. Zavattaro. On the power of cliques in the parameterized verification of ad hoc networks. In FOSSACS, volume 6604 of LNCS, pages 441--455. Springer, 2011."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-30793-5_15"},{"key":"e_1_2_1_22_1","series-title":"LNCS","first-page":"516","volume-title":"CAV","author":"Elgaard J.","year":"1998","unstructured":"J. Elgaard , N. Klarlund , and A. M\u00f8ller . MONA 1.x: new techniques for WS1S and WS2S . In CAV , volume 1427 of LNCS , pages 516 -- 520 . Springer , 1998 . J. Elgaard, N. Klarlund, and A. M\u00f8ller. MONA 1.x: new techniques for WS1S and WS2S. In CAV, volume 1427 of LNCS, pages 516--520. Springer, 1998."},{"key":"e_1_2_1_23_1","series-title":"LNCS","first-page":"236","volume-title":"CADE","author":"Emerson E. A.","year":"2000","unstructured":"E. A. Emerson and V. Kahlon . Reducing model checking of the many to the few . In CADE , volume 1831 of LNCS , pages 236 -- 254 . Springer Berlin Heidelberg , 2000 . E. A. Emerson and V. Kahlon. Reducing model checking of the many to the few. In CADE, volume 1831 of LNCS, pages 236--254. Springer Berlin Heidelberg, 2000."},{"key":"e_1_2_1_24_1","series-title":"LNCS","first-page":"247","volume-title":"CHARME","author":"Emerson E. A.","year":"2003","unstructured":"E. A. Emerson and V. Kahlon . Exact and efficient verification of parameterized cache coherence protocols . In CHARME , volume 2860 of LNCS , pages 247 -- 262 . Springer , 2003 . E. A. Emerson and V. Kahlon. Exact and efficient verification of parameterized cache coherence protocols. In CHARME, volume 2860 of LNCS, pages 247--262. Springer, 2003."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2003.1210076"},{"key":"e_1_2_1_26_1","series-title":"LNCS","first-page":"87","volume-title":"CAV","author":"Emerson E. A.","year":"1996","unstructured":"E. A. Emerson and K. S. Namjoshi . Automatic verification of parameterized synchronous systems . In CAV , volume 1102 of LNCS , pages 87 -- 98 . Springer , 1996 . E. A. Emerson and K. S. Namjoshi. Automatic verification of parameterized synchronous systems. In CAV, volume 1102 of LNCS, pages 87--98. Springer, 1996."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0129054103001881"},{"key":"e_1_2_1_28_1","doi-asserted-by":"crossref","first-page":"374","DOI":"10.1007\/3-540-65306-6_20","volume-title":"Lectures on Petri Nets I: Basic Models","author":"Esparza J.","year":"1998","unstructured":"J. Esparza . Decidability and complexity of petri net problems - an introduction. In In Lectures on Petri Nets I: Basic Models , pages 374 -- 428 . Springer-Verlag , 1998 . J. Esparza. Decidability and complexity of petri net problems - an introduction. In In Lectures on Petri Nets I: Basic Models, pages 374--428. Springer-Verlag, 1998."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00102-X"},{"key":"e_1_2_1_30_1","volume-title":"Backward reachability of array-based systems by SMT solving: Termination and invariant synthesis. Logical Methods in Computer Science, 6(4)","author":"Ghilardi S.","year":"2010","unstructured":"S. Ghilardi and S. Ranise . Backward reachability of array-based systems by SMT solving: Termination and invariant synthesis. Logical Methods in Computer Science, 6(4) , 2010 . S. Ghilardi and S. Ranise. Backward reachability of array-based systems by SMT solving: Termination and invariant synthesis. Logical Methods in Computer Science, 6(4), 2010."},{"key":"e_1_2_1_31_1","series-title":"LNCS","first-page":"928","volume-title":"CAV","author":"Khalimov A.","year":"2013","unstructured":"A. Khalimov , S. Jacobs , and R. Bloem . PARTY parameterized synthesis of token rings . In CAV , volume 8044 of LNCS , pages 928 -- 933 . Springer , 2013 . A. Khalimov, S. Jacobs, and R. Bloem. PARTY parameterized synthesis of token rings. In CAV, volume 8044 of LNCS, pages 928--933. Springer, 2013."},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2008.11.006"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_52"},{"key":"e_1_2_1_34_1","volume-title":"Distributed Algorithms","author":"Lynch N.","year":"1996","unstructured":"N. Lynch . Distributed Algorithms . Morgan Kaufman Publishers, Inc. , San Francisco, USA , 1996 . N. Lynch. Distributed Algorithms. Morgan Kaufman Publishers, Inc., San Francisco, USA, 1996."},{"key":"e_1_2_1_35_1","volume-title":"VAS -- Verification of autonomous systems","author":"P.","year":"2016","unstructured":"MCMAS- P. VAS -- Verification of autonomous systems , 2016 . URL : http:\/\/vas.doc.ic.ac.uk\/software\/extensions\/. Accessed : April 2016. MCMAS-P. VAS -- Verification of autonomous systems, 2016. URL: http:\/\/vas.doc.ic.ac.uk\/software\/extensions\/. Accessed: April 2016."},{"key":"e_1_2_1_36_1","volume-title":"PHI Series in computer science","author":"Milner R.","year":"1989","unstructured":"R. Milner . Communication and concurrency. PHI Series in computer science . Prentice Hall , 1989 . R. Milner. Communication and concurrency. PHI Series in computer science. Prentice Hall, 1989."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_18"},{"key":"e_1_2_1_38_1","series-title":"LNCS","first-page":"184","volume-title":"CAV","author":"Pnueli A.","year":"1996","unstructured":"A. Pnueli and E. Shahar . A platform for combining deductive with algorithmic verification . In CAV , volume 1102 of LNCS , pages 184 -- 195 . Springer , 1996 . A. Pnueli and E. Shahar. A platform for combining deductive with algorithmic verification. In CAV, volume 1102 of LNCS, pages 184--195. Springer, 1996."},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(95)00017-8"},{"key":"e_1_2_1_40_1","series-title":"LNCS","first-page":"489","volume-title":"AMAST","author":"Rybina T.","year":"2002","unstructured":"T. Rybina and A. Voronkov . BRAIN : Backward reachability analysis with integers . In AMAST , volume 2422 of LNCS , pages 489 -- 494 . Springer , 2002 . T. Rybina and A. Voronkov. BRAIN : Backward reachability analysis with integers. In AMAST, volume 2422 of LNCS, pages 489--494. Springer, 2002."},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(88)90211-6"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-009-0081-1"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.cl.2004.02.006"}],"container-title":["ACM SIGACT News"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2951860.2951873","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2951860.2951873","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T03:39:36Z","timestamp":1750217976000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2951860.2951873"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,6,3]]},"references-count":43,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2016,6,3]]}},"alternative-id":["10.1145\/2951860.2951873"],"URL":"https:\/\/doi.org\/10.1145\/2951860.2951873","relation":{},"ISSN":["0163-5700"],"issn-type":[{"value":"0163-5700","type":"print"}],"subject":[],"published":{"date-parts":[[2016,6,3]]},"assertion":[{"value":"2016-06-03","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}