{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,1]],"date-time":"2026-02-01T11:41:33Z","timestamp":1769946093827,"version":"3.49.0"},"reference-count":52,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2015,11,23]],"date-time":"2015-11-23T00:00:00Z","timestamp":1448236800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2016,10]]},"DOI":"10.1007\/s10009-015-0406-x","type":"journal-article","created":{"date-parts":[[2015,11,23]],"date-time":"2015-11-23T10:55:34Z","timestamp":1448276134000},"page":"495-516","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":39,"title":["Parameterized verification through view abstraction"],"prefix":"10.1007","volume":"18","author":[{"given":"Parosh","family":"Abdulla","sequence":"first","affiliation":[]},{"given":"Fr\u00e9d\u00e9ric","family":"Haziza","sequence":"additional","affiliation":[]},{"given":"Luk\u00e1\u0161","family":"Hol\u00edk","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,11,23]]},"reference":[{"issue":"4","key":"406_CR1","doi-asserted-by":"crossref","first-page":"457","DOI":"10.2178\/bsl\/1294171129","volume":"16","author":"PA Abdulla","year":"2010","unstructured":"Abdulla, P.A.: Well (and better) quasi-ordered transition systems. Bull. Symb. Logic 16(4), 457\u2013515 (2010)","journal-title":"Bull. Symb. Logic"},{"key":"406_CR2","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., \u010cer\u0101ns, K., Jonsson, B., Tsay, Y.-K.: General decidability theorems for infinite-state systems. In: LICS\u201996, pp. 313\u2013321 (1996)","DOI":"10.1109\/LICS.1996.561359"},{"key":"406_CR3","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Delzanno, G., Rezine, A.: Approximated context-sensitive analysis for parameterized verification. In: Lee, D., Lopes, A., Poetzsch-Heffter, A. (eds.) FORTE\u201909, vol. 5522 of LNCS, pp. 41\u201356. Springer (2009)","DOI":"10.1007\/978-3-642-02138-1_3"},{"key":"406_CR4","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Haziza, F., Hol\u00edk, L.: Block me if you can!\u2014context-sensitive parameterized verification. In: SAS14, pp. 1\u201317 (2014)","DOI":"10.1007\/978-3-319-10936-7_1"},{"key":"406_CR5","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Haziza, F., Hol\u00edk, L., Jonsson, B., Rezine, A.: An integrated specification and verification technique for highly concurrent data structures. In: TACAS13, pp. 324\u2013338 (2013)","DOI":"10.1007\/978-3-642-36742-7_23"},{"key":"406_CR6","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Haziza, F., Hol\u00edk, L.: All for the price of few (parameterized verification through view abstraction). In: Proceedings of VMCAI \u201913, 14th International Conference on Verification, Model Checking, and Abstract Interpretation, vol. 7737 of LNCS, pp. 476\u2013495 (2013)","DOI":"10.1007\/978-3-642-35873-9_28"},{"key":"406_CR7","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Henda, N.B., Delzanno, G., Rezine, A.: Regular model checking without transducers (on efficient verification of parameterized systems). In: TACAS\u201907, vol. 4424 of LNCS, pp. 721\u2013736. Springer (2007)","DOI":"10.1007\/978-3-540-71209-1_56"},{"key":"406_CR8","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Henda, N.B., Delzanno, G., Rezine, A.: Handling parameterized systems with non-atomic global conditions. In: VMCAI08, vol. 4905 of LNCS, pp. 22\u201336. Springer (2008)","DOI":"10.1007\/978-3-540-78163-9_7"},{"key":"406_CR9","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Jonsson, B.: Verifying programs with unreliable channels. In: Proc. LICS \u201993, 8th IEEE Int. Symp. on Logic in Computer Science, pp. 160\u2013170 (1993)","DOI":"10.1109\/LICS.1993.287591"},{"key":"406_CR10","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Jonsson, B., Nilsson, M., d\u2019Orso, J.: Regular model checking made simple and efficient. In: Proc. CONCUR \u201902, 13th International Conference on Concurrency Theory, vol. 2421 of LNCS, pp. 116\u2013130. Springer (2002)","DOI":"10.1007\/3-540-45694-5_9"},{"key":"406_CR11","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., \u010cer\u0101ns, K., Jonsson, B., Tsay, Y.-K.: Algorithmic analysis of programs with well quasi-ordered domains. Inf. Comput. 160(1\u20132), 109\u2013127 (2000)","DOI":"10.1006\/inco.1999.2843"},{"key":"406_CR12","unstructured":"Alberti, F., Ghilardi, S., Sharygina, N.: A framework for the verification of parameterized infinite-state systems. In: Proceedings of the 29th Italian Conference on Computational Logic, vol. 1195 of CEUR Workshop Proceedings, pp. 303\u2013308. CEUR-WS.org (2014)"},{"key":"406_CR13","doi-asserted-by":"crossref","unstructured":"Arons, T., Pnueli, A., Ruah, S. Xu, J., Zuck, L.: Parameterized verification with automatically computed inductive assertions. In: CAV\u201901, vol. 2102 of LNCS, pp. 221\u2013234. Springer (2001)","DOI":"10.1007\/3-540-44585-4_19"},{"issue":"1","key":"406_CR14","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1007\/s10009-002-0095-0","volume":"5","author":"T Ball","year":"2003","unstructured":"Ball, T., Podelski, A., Rajamani, S.K.: Boolean and cartesian abstraction for model checking C programs. STTT 5(1), 49\u201358 (2003)","journal-title":"STTT"},{"key":"406_CR15","doi-asserted-by":"crossref","unstructured":"Baukus, K., Lakhnech, Y., Stahl, K.: Parameterized verification of a cache coherence protocol: Safety and liveness. In: VMCAI02, vol. 2294 of LNCS, pp 317\u2013330. Springer (2002)","DOI":"10.1007\/3-540-47813-2_22"},{"key":"406_CR16","doi-asserted-by":"crossref","unstructured":"Bingham, J.D., Hu, A.J.: Empirically efficient verification for a class of infinite-state systems. In: TACAS\u201905, vol. 3440 of LNCS, pp. 77\u201392. Springer (2005)","DOI":"10.1007\/978-3-540-31980-1_6"},{"key":"406_CR17","doi-asserted-by":"crossref","unstructured":"Boigelot, B., Legay, A., Wolper, P.: Iterating transducers in the large. In: CAV\u201903, vol. 2725 of LNCS, pp. 223\u2013235. Springer (2003)","DOI":"10.1007\/978-3-540-45069-6_24"},{"key":"406_CR18","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Habermehl, P., Vojnar, T.: Abstract regular model checking. In: CAV\u201904, vol. 3114 of LNCS, pp. 372\u2013386. Springer (2004)","DOI":"10.1007\/978-3-540-27813-9_29"},{"key":"406_CR19","doi-asserted-by":"crossref","unstructured":"Clarke, E., Talupur, M., Veith, H.: Environment abstraction for parameterized verification. In: VMCAI\u201906, vol. 3855 of LNCS, pp. 126\u2013141. Springer (2006)","DOI":"10.1007\/11609773_9"},{"key":"406_CR20","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Emerson, A.E.: Design and synthesis of synchronization skeletons using branching-time temporal logic. Logic of Programs. Workshop, pp. 52\u201371. UK, UK, Springer-Verlag, London (1982)","DOI":"10.1007\/BFb0025774"},{"key":"406_CR21","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Talupur, M., Veith, H.: Environment abstraction for parameterized verification. In: VMCAI06, vol. 3855 of LNCS, pp. 126\u2013141. Springer (2006)","DOI":"10.1007\/11609773_9"},{"key":"406_CR22","doi-asserted-by":"crossref","unstructured":"Dams, D., Lakhnech, Y., Steffen, M.: Iterating transducers. In: CAV\u201901, vol. 2102 of LNCS. Springer (2001)","DOI":"10.1007\/3-540-44585-4_27"},{"key":"406_CR23","doi-asserted-by":"crossref","unstructured":"Delzanno, G.: Automatic verification of cache coherence protocols. In: Emerson, Sistla (eds.) CAV\u201900, vol. 1855 of LNCS, pp. 53\u201368. Springer (2000)","DOI":"10.1007\/10722167_8"},{"key":"406_CR24","doi-asserted-by":"crossref","unstructured":"Delzanno, G.: Verification of consistency protocols via infinite-state symbolic model checking. In: FORTE\u201900, vol. 183 of IFIP Conference Proceedings, pp. 171\u2013186. Kluwer (2000)","DOI":"10.1007\/978-0-387-35533-7_11"},{"key":"406_CR25","doi-asserted-by":"crossref","unstructured":"Delzanno, G., Raskin, J.-F.: Symbolic representation of upward-closed sets. In: TACAS\u201900, vol. 1785 of LNCS, pp. 426\u2013441. Springer (2000)","DOI":"10.1007\/3-540-46419-0_29"},{"key":"406_CR26","unstructured":"Delzanno, G., Raskin, J.-F., Van Begin, L.: Csts (covering sharing trees): Compact data structures for parameterized verification. In: Software Tools for Technology Transfer (2001)"},{"key":"406_CR27","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Kahlon, V.: Reducing model checking of the many to the few. In: CADE\u201900, vol. 1831 of LNCS, pp. 236\u2013254. Springer (2000)","DOI":"10.1007\/10721959_19"},{"key":"406_CR28","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Namjoshi, K.S.: Reasoning about rings. In: POPL\u201995, pp. 85\u201394 (1995)","DOI":"10.1145\/199448.199468"},{"key":"406_CR29","doi-asserted-by":"crossref","unstructured":"Esparza, J., Finkel, A., Mayr, R.: On the verification of broadcast protocols. In: LICS\u201999. IEEE Computer Society (1999)","DOI":"10.1109\/LICS.1999.782630"},{"key":"406_CR30","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Qadeer, S.: Thread-modular model checking. In: SPIN\u201903, vol. 2648 of LNCS, pp. 213\u2013224. Springer (2003)","DOI":"10.1007\/3-540-44829-2_14"},{"key":"406_CR31","unstructured":"Ganty, P., Meuter, C., Delzanno, G., Kalyon, G., Raskin, J.-F., Van Begin, L.: Symbolic data structure for sets of $$k$$ k -uples. Technical Report 570, Universit\u00e9 Libre de Bruxelles, Belgium (2007)"},{"key":"406_CR32","doi-asserted-by":"crossref","unstructured":"Ganty, P., Raskin, J.-F., Van Begin, L.: A Complete Abstract Interpretation Framework for Coverability Properties of WSTS. In: VMCAI06, vol. 3855 of LNCS, pp. 49\u201364. Springer (2006)","DOI":"10.1007\/11609773_4"},{"key":"406_CR33","doi-asserted-by":"crossref","unstructured":"Geeraerts, G., Raskin, J.-F., Van Begin, L.: Expand, enlarge and check... made efficient. In: CAV\u201905, vol. 3576 of LNCS, pp. 394\u2013407. Springer (2005)","DOI":"10.1007\/11513988_38"},{"issue":"1","key":"406_CR34","doi-asserted-by":"crossref","first-page":"180","DOI":"10.1016\/j.jcss.2005.09.001","volume":"72","author":"G Geeraerts","year":"2006","unstructured":"Geeraerts, G., Raskin, J.-F., Van Begin, L.: Expand, enlarge and check: new algorithms for the coverability problem of WSTS. J. Comput. Syst. Sci. 72(1), 180\u2013203 (2006)","journal-title":"J. Comput. Syst. Sci."},{"issue":"3","key":"406_CR35","doi-asserted-by":"crossref","first-page":"675","DOI":"10.1145\/146637.146681","volume":"39","author":"SM German","year":"1992","unstructured":"German, S.M., Sistla, A.P.: Reasoning about systems with many processes. J ACM 39(3), 675\u2013735 (1992)","journal-title":"J ACM"},{"key":"406_CR36","doi-asserted-by":"crossref","unstructured":"Ghilardi, S., Nicolini, E., Ranise, S., Zucchelli, D.: Towards smt model checking of array-based systems. In: Automated Reasoning, vol. 5195 of LNCS, pp. 67\u201382. Springer (2008)","DOI":"10.1007\/978-3-540-71070-7_6"},{"key":"406_CR37","unstructured":"Haziza, F.: Experiments | parameterized verification through view abstraction. http:\/\/www.it.uu.se\/research\/docs\/fm\/apv\/parametrized\/experiments\/ (2013)"},{"issue":"5","key":"406_CR38","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"GJ Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker spin. IEEE Trans. Softw. Eng. 23(5), 279\u2013295 (1997)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"406_CR39","unstructured":"IEEE\u00a0Computer\u00a0Society. IEEE standard for a high performance serial bus. Std 1394\u20131995 (1996)"},{"key":"406_CR40","doi-asserted-by":"crossref","unstructured":"Kaiser, A., Kroening, D., Wahl, T.: Dynamic cutoff detection in parameterized concurrent programs. In: CAV\u201910, vol. 6174 of LNCS, pp. 645\u2013659. Springer (2010)","DOI":"10.1007\/978-3-642-14295-6_55"},{"key":"406_CR41","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1016\/S0304-3975(00)00103-1","volume":"256","author":"Y Kesten","year":"2001","unstructured":"Kesten, Y., Maler, O., Marcus, M., Pnueli, A., Shahar, E.: Symbolic model checking with rich assertional languages. Theor. Comput. Sci. 256, 93\u2013112 (2001)","journal-title":"Theor. Comput. Sci."},{"key":"406_CR42","unstructured":"Lynch, N.A., Shamir, B.-P.: Distributed algorithms, lecture notes for 6.852, fall 1992. Technical Report MIT\/LCS\/RSS-20, MIT (1993)"},{"key":"406_CR43","doi-asserted-by":"crossref","unstructured":"Malkis, A., Podelski, A., Rybalchenko, A.: Thread-modular verification is cartesian abstract interpretation. In: ICTAC\u201906, vol. 4281 of LNCS, pp. 183\u2013197. Springer (2006)","DOI":"10.1007\/11921240_13"},{"key":"406_CR44","doi-asserted-by":"crossref","unstructured":"Malkis, A., Podelski, A., Rybalchenko, A.: Precise thread-modular verification. In: SAS\u201907, vol. 4634 of LNCS, pp. 218\u2013232. Springer (2007)","DOI":"10.1007\/978-3-540-74061-2_14"},{"key":"406_CR45","doi-asserted-by":"crossref","unstructured":"Namjoshi, K.S.: Symmetry and completeness in the analysis of parameterized systems. In: VMCAI07, vol. 4349 of LNCS, pp. 299\u2013313. Springer (2007)","DOI":"10.1007\/978-3-540-69738-1_22"},{"key":"406_CR46","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Xu, J., Zuck, L.: Liveness with (0,1,infinity)-counter abstraction. In: CAV\u201902, vol. 2404 of LNCS. Springer (2002)","DOI":"10.1007\/3-540-45657-0_9"},{"key":"406_CR47","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Ruah, S., Zuck, L.D.: Automatic deductive verification with invisible invariants. In: TACAS\u201901, vol. 2031 of LNCS, pp. 82\u201397. Springer (2001)","DOI":"10.1007\/3-540-45319-9_7"},{"key":"406_CR48","doi-asserted-by":"crossref","unstructured":"Queille, J.-P., Sifakis, J.: Specification and verification of concurrent systems in cesar. In: Proceedings of the 5th Colloquium on International Symposium on Programming, pp. 337\u2013351, London, UK, UK, Springer-Verlag (1982)","DOI":"10.1007\/3-540-11494-7_22"},{"key":"406_CR49","doi-asserted-by":"crossref","unstructured":"Szymanski, B.K.: A simple solution to lamport\u2019s concurrent programming problem with linear wait. Proceedings of the 2nd International Conference on Supercomputing. ICS \u201988, pp. 621\u2013626. NY, USA, ACM, New York (1988)","DOI":"10.1145\/55364.55425"},{"key":"406_CR50","doi-asserted-by":"crossref","unstructured":"Szymanski, B.K.: Mutual exclusion revisited. In: Proc. Fifth Jerusalem Conference on Information Technology, IEEE Computer Society Press, Los Alamitos, CA, pp. 110\u2013117. IEEE Computer Society Press (1990)","DOI":"10.1109\/JCIT.1990.128275"},{"key":"406_CR51","doi-asserted-by":"crossref","unstructured":"Touili, T.: Regular Model Checking using Widening Techniques. Electronic Notes in Theoretical Computer Science, 50(4), (2001) Proc. of VEPAS\u201901","DOI":"10.1016\/S1571-0661(04)00187-2"},{"key":"406_CR52","unstructured":"Vojnar, T.: Private communication, June (1993)"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-015-0406-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-015-0406-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-015-0406-x","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,1]],"date-time":"2019-09-01T20:13:13Z","timestamp":1567368793000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-015-0406-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,11,23]]},"references-count":52,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2016,10]]}},"alternative-id":["406"],"URL":"https:\/\/doi.org\/10.1007\/s10009-015-0406-x","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,11,23]]}}}