{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,4]],"date-time":"2023-09-04T23:10:45Z","timestamp":1693869045990},"reference-count":47,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2015,2,25]],"date-time":"2015-02-25T00:00:00Z","timestamp":1424822400000},"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":["Acta Informatica"],"published-print":{"date-parts":[[2015,9]]},"DOI":"10.1007\/s00236-015-0222-5","type":"journal-article","created":{"date-parts":[[2015,2,24]],"date-time":"2015-02-24T13:55:57Z","timestamp":1424786157000},"page":"525-557","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Parametrized invariance for infinite state processes"],"prefix":"10.1007","volume":"52","author":[{"given":"Alejandro","family":"S\u00e1nchez","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"C\u00e9sar","family":"S\u00e1nchez","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,2,25]]},"reference":[{"key":"222_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Bouajjani, A., Jonsson, B., Nilsson, M.: Handling global conditions in parametrized system verification. In: Proceedings of CAV\u201999. pp. 134\u2013145 (1999)","DOI":"10.1007\/3-540-48683-6_14"},{"key":"222_CR2","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.K.: General decidability theorems for infinite-state systems. In: Proceedings of LICS\u201996. pp. 313\u2013321. IEEE Computer Society (1996)","DOI":"10.1109\/LICS.1996.561359"},{"issue":"2","key":"222_CR3","first-page":"126","volume":"34","author":"PA Abdulla","year":"2009","unstructured":"Abdulla, P.A., Delzanno, G., Rezine, A.: Approximated parameterized verification of infinite-state processes with global conditions. FMSD 34(2), 126\u2013156 (2009)","journal-title":"FMSD"},{"key":"222_CR4","doi-asserted-by":"crossref","unstructured":"Amit, D., Rinetzky, N., Reps, T.W., Sagiv, M., Yahav, E.: Comparison under abstraction for verifying linearizability. In: Proceedings of CAV\u201907. LNCS, vol. 4590, pp. 477\u2013490. Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-73368-3_49"},{"issue":"6","key":"222_CR5","doi-asserted-by":"crossref","first-page":"307","DOI":"10.1016\/0020-0190(86)90071-2","volume":"22","author":"KR Apt","year":"1986","unstructured":"Apt, K.R., Kozen, D.C.: Limits for automatic verification of finite-state concurrent systems. Inf. Process. Lett. 22(6), 307\u2013309 (1986)","journal-title":"Inf. Process. Lett."},{"key":"222_CR6","doi-asserted-by":"crossref","unstructured":"Arons, T., Pnueli, A., Ruah, S., Xu, J., Zuck, L.D.: Parameterized verification with automatically computed inductive assertions. In: Proceedings of CAV\u201901. LNCS, vol. 2102, pp. 221\u2013234. Springer, Berlin (2001)","DOI":"10.1007\/3-540-44585-4_19"},{"key":"222_CR7","doi-asserted-by":"crossref","unstructured":"Berdine, J., Lev-Ami, T., Manevich, R., Ramalingam, G., Sagiv, S.: Thread quantification for concurrent shape analysis. In: Proceedings of CAV\u201908. LNCS, vol. 5123, pp. 399\u2013413. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-70545-1_37"},{"key":"222_CR8","doi-asserted-by":"crossref","unstructured":"Bradley, A.R.: SAT-based model checking without unrolling. In: Proceedings of VMCAI\u201911. LNCS, vol. 6538, pp. 70\u201387. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"222_CR9","doi-asserted-by":"crossref","unstructured":"Bradley, A.R., Manna, Z., Sipma., H.B.: What\u2019s decidable about arrays? In: Proceedings of VMCAI\u201906. LNCS, vol. 3855, pp. 427\u2013442. Springer, Berlin (2006)","DOI":"10.1007\/11609773_28"},{"key":"222_CR10","doi-asserted-by":"crossref","unstructured":"Browne, A., Manna, Z., Sipma, H.B.: Generalized verification diagrams. In: Proceedings of FSTTCS\u201995. LNCS, vol. 1206, pp. 484\u2013498. Springer, Berlin (1995)","DOI":"10.1007\/3-540-60692-0_69"},{"key":"222_CR11","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O.: Avoiding the state explosion problem in temporal logic model checking. In: Proceedings of PODC\u201987. pp. 294\u2013303. ACM, New York (1987)","DOI":"10.1145\/41840.41865"},{"key":"222_CR12","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., Browne, M.C.: Reasoning about networks with many identical finite-state processes. In: PODC\u201986, pp. 240\u2013248. ACM, New York (1986)","DOI":"10.1145\/10590.10611"},{"issue":"1\/2","key":"222_CR13","first-page":"77","volume":"9","author":"EM Clarke","year":"1996","unstructured":"Clarke, E.M., Jha, S., Enders, R., Filkorn, T.: Exploiting symmetry in temporal logic model checking. FMSD 9(1\/2), 77\u2013104 (1996)","journal-title":"FMSD"},{"key":"222_CR14","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Talupur, M., Veith, H.: Proving ptolemy right: the environment abstraction framework for model checking concurrent systems. In: Proceedings of TACAS\u201908. LNCS, vol. 4963, pp. 33\u201347. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-78800-3_4"},{"key":"222_CR15","doi-asserted-by":"crossref","unstructured":"Dutertre, B.: Yices 2.2. In: Proceedings of CAV\u201914, LNCS, vol. 8559, pp. 737\u2013744. Springer, Berlin (2014)","DOI":"10.1007\/978-3-319-08867-9_49"},{"key":"222_CR16","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Kahlon, V.: Reducing model checking of the many to the few. In: Proceedings of CADE\u201900, LNAI, vol. 1831, pp. 236\u2013254. Springer, Berlin (2000)","DOI":"10.1007\/10721959_19"},{"key":"222_CR17","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Namjoshi, K.S.: Reasoning about rings. In: Proceedings of POPL\u201995, pp. 85\u201394. ACM, New York (1995)","DOI":"10.1145\/199448.199468"},{"key":"222_CR18","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Namjoshi, K.S.: Automatic verification of parameterized synchronous systems. In: Proceedings of CAV\u201996, LNCS, vol. 1102, pp. 87\u201398. Springer, Berlin (1996)","DOI":"10.1007\/3-540-61474-5_60"},{"issue":"1\/2","key":"222_CR19","first-page":"105","volume":"9","author":"EA Emerson","year":"1996","unstructured":"Emerson, E.A., Sistla, A.P.: Symmetry and model checking. FMSD 9(1\/2), 105\u2013131 (1996)","journal-title":"FMSD"},{"key":"222_CR20","doi-asserted-by":"crossref","unstructured":"Fontaine, P., Ranise, S., Zarba, C.G.: Combining lists with non-stably infinite theories. In: Proceedings of LPAR\u201904, pp. 51\u201366. Springer, Berlin (2004)","DOI":"10.1007\/978-3-540-32275-7_4"},{"key":"222_CR21","doi-asserted-by":"crossref","unstructured":"Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): Fast decision procedures. In: Proceedings of CAV\u201904, LNCS, vol. 3114, pp. 175\u2013188. Springer, Berlin (2004)","DOI":"10.1007\/978-3-540-27813-9_14"},{"issue":"3","key":"222_CR22","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":"222_CR23","doi-asserted-by":"crossref","unstructured":"Grebenshchikov, S., Lopes, N.P., Popeea, C., Rybalchenko, A.: Synthesizing software verifiers from proof rules. In: Proceedings of PLDI\u201912, pp. 415\u2013416. ACM, New York (2012)","DOI":"10.1145\/2254064.2254112"},{"key":"222_CR24","unstructured":"Herlihy, M., Shavit, N.: The Art of Multiprocessor Programming. Morgran-Kaufmann, Burlington (2008)"},{"key":"222_CR25","doi-asserted-by":"crossref","unstructured":"Hoder, K., Bj\u00f8rner, N.: Generalized property directed reachability. In: Proceedings of SAT\u201912, LNCS, vol. 7317, pp. 157\u2013171. Springer, Berlin (2012)","DOI":"10.1007\/978-3-642-31612-8_13"},{"key":"222_CR26","doi-asserted-by":"crossref","unstructured":"Kesten, Y., Pnueli, A., on Raviv, L.: Algorithmic verification of linear temporal logic specifications. In: Proceedings of ICALP\u201998, LNCS, vol. 1443, pp. 1\u201316. Springer, Berlin (1998)","DOI":"10.1007\/BFb0055036"},{"key":"222_CR27","doi-asserted-by":"crossref","unstructured":"Lahiri, S.K., Qadeer, S.: Back to the future: revisiting precise program verification using SMT solvers. In: Proceedings of POPL\u201908. pp. 171\u2013182. ACM, New York (2008)","DOI":"10.1145\/1328438.1328461"},{"key":"222_CR28","doi-asserted-by":"crossref","unstructured":"Lesens, D., Halbwachs, N., Raymond, P.: Automatic verification of parameterized linear networks of processes. In: Proceedings of POPL\u201997. pp. 346\u2013357. ACM, New York (1997)","DOI":"10.1145\/263699.263747"},{"key":"222_CR29","doi-asserted-by":"crossref","unstructured":"Madhusudan, P., Parlato, G., Qiu, X.: Decidable logics combining heap structures and data. In: Proceedings of POPL\u201911, pp. 611\u2013622. ACM, New York (2011)","DOI":"10.1145\/1926385.1926455"},{"key":"222_CR30","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, Berlin (1995)","DOI":"10.1007\/978-1-4612-4222-2"},{"key":"222_CR31","doi-asserted-by":"crossref","unstructured":"Marco Bozzano, G.D.: Beyond parameterized verification. In: TACAS\u201902. LNCS, vol. 2280, pp. 221\u2013235. Springer, Berlin (2002)","DOI":"10.1007\/3-540-46002-0_16"},{"key":"222_CR32","doi-asserted-by":"crossref","unstructured":"Michael, M.M., Scott, M.L.: Simple, fast, and practical non-blocking and blocking concurrent queue algorithms. In: Proceedings of PODC\u201996, pp. 267\u2013275 (1996)","DOI":"10.1145\/248052.248106"},{"key":"222_CR33","doi-asserted-by":"crossref","unstructured":"de Moura, L.M., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Proceedings of TACAS\u201908, LNCS, vol. 4963, pp. 337\u2013340. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"222_CR34","doi-asserted-by":"crossref","unstructured":"Nelson, C.G., Oppen, D.C.: A simplifier based on efficient decision algorithms. In: Proceedings of POPL\u201978, pp. 141\u2013150. ACM, New York (1978)","DOI":"10.1145\/512760.512775"},{"key":"222_CR35","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Ruah, S., Zuck, L.D.: Automatic deductive verification with invisible invariants. In: Proceedings of TACAS\u201901, LNCS, vol. 2031, pp. 82\u201397. Springer, Berlin (2001)","DOI":"10.1007\/3-540-45319-9_7"},{"key":"222_CR36","doi-asserted-by":"crossref","unstructured":"Qiu, X., Garg, P., Stefanescu, A., Madhusudan, P.: Natural proofs for structure, data, and separation. In: Proceedings of PLDI\u201913, pp. 231\u2013242. ACM, New York (2013)","DOI":"10.1145\/2491956.2462169"},{"key":"222_CR37","doi-asserted-by":"crossref","unstructured":"S\u00e1nchez, A., S\u00e1nchez, C.: Decision procedures for the temporal verification of concurrent lists. In: Proceedings of ICFEM\u201910, LNCS, vol. 6447, pp. 74\u201389. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-16901-4_7"},{"key":"222_CR38","doi-asserted-by":"crossref","unstructured":"S\u00e1nchez, A., S\u00e1nchez, C.: Parametrized verification diagrams. In: Proceedings of TIME\u201914, pp. 132\u2013141. IEEE Computer Society Press, Los Alamitos (2014)","DOI":"10.1109\/TIME.2014.11"},{"key":"222_CR39","doi-asserted-by":"crossref","unstructured":"S\u00e1nchez, A., Sankaranarayanan, S., S\u00e1nchez, C., Chang, B.Y.E.: Invariant generation for parametrized systems using self-reflection. In: Proceedings of SAS\u201912, LNCS, vol. 7460, pp. 146\u2013163. Springer, Berlin (2012)","DOI":"10.1007\/978-3-642-33125-1_12"},{"key":"222_CR40","doi-asserted-by":"crossref","unstructured":"Sofronie-Stokkermans, V.: Hierarchic reasoning in local theory extensions. In: Proceedings of CADE\u201905, LNCS, vol. 3632, pp. 219\u2013234. Springer, Berlin (2005)","DOI":"10.1007\/11532231_16"},{"key":"222_CR41","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1016\/0020-0190(88)90211-6","volume":"28","author":"I Suzuki","year":"1988","unstructured":"Suzuki, I.: Proving properties of a ring of finite-state machines. Inf. Process. Lett. 28, 213\u2013214 (1988)","journal-title":"Inf. Process. Lett."},{"key":"222_CR42","doi-asserted-by":"crossref","unstructured":"Tinelli, C., Zarba, C.G.: Combining decision procedures for sorted theories. In: Proceedings Logic in Artificial Intelligence (JELIA\u201904), LNCS, vol. 3229, pp. 641\u2013653. Springer, Berlin (2004)","DOI":"10.1007\/978-3-540-30227-8_53"},{"key":"222_CR43","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1007\/s10817-005-5204-9","volume":"34","author":"C Tinelli","year":"2005","unstructured":"Tinelli, C., Zarba, C.G.: Combining nonstably infinite theories. J. Autom. Reas. 34, 209\u2013238 (2005)","journal-title":"J. Autom. Reas."},{"key":"222_CR44","doi-asserted-by":"crossref","unstructured":"Totla, N., Wies, T.: Complete instantiation-based interpolation. In: Proceedings of POPL\u201913, pp. 537\u2013548. ACM, New York (2013)","DOI":"10.1145\/2429069.2429132"},{"key":"222_CR45","doi-asserted-by":"crossref","unstructured":"Vafeiadis, V.: Shape-value abstraction for verifying linearizability. In: VMCAI. Lecture Notes in Computer Science, vol. 5403, pp. 335\u2013348. Springer, Berlin (2009)","DOI":"10.1007\/978-3-540-93900-9_27"},{"key":"222_CR46","doi-asserted-by":"crossref","unstructured":"Vafeiadis, V.: Automatically proving linearizability. In: Proceedings of CAV\u201910, LNCS, vol. 6174, pp. 450\u2013464. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-14295-6_40"},{"key":"222_CR47","first-page":"139","volume":"30","author":"LD Zuck","year":"2004","unstructured":"Zuck, L.D., Pnueli, A.: Model checking and abstraction to the aid of parameterized systems (a survey). Comput. Lang. Syst. Struct. 30, 139\u2013169 (2004)","journal-title":"Comput. Lang. Syst. Struct."}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-015-0222-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00236-015-0222-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-015-0222-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,21]],"date-time":"2019-08-21T05:51:43Z","timestamp":1566366703000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00236-015-0222-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,2,25]]},"references-count":47,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2015,9]]}},"alternative-id":["222"],"URL":"https:\/\/doi.org\/10.1007\/s00236-015-0222-5","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"value":"0001-5903","type":"print"},{"value":"1432-0525","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,2,25]]}}}