{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T04:09:04Z","timestamp":1749787744398,"version":"3.41.0"},"reference-count":57,"publisher":"Springer Science and Business Media LLC","issue":"3-4","license":[{"start":{"date-parts":[[2016,11,15]],"date-time":"2016-11-15T00:00:00Z","timestamp":1479168000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Ann Math Artif Intell"],"published-print":{"date-parts":[[2017,8]]},"DOI":"10.1007\/s10472-016-9531-9","type":"journal-article","created":{"date-parts":[[2016,11,17]],"date-time":"2016-11-17T07:42:45Z","timestamp":1479368565000},"page":"249-282","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Parametrized verification diagrams: temporal verification of symmetric parametrized concurrent systems"],"prefix":"10.1007","volume":"80","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":[[2016,11,15]]},"reference":[{"issue":"6","key":"9531_CR1","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. Proc. Letters 22(6), 307\u2013309 (1986)","journal-title":"Inf. Proc. Letters"},{"key":"9531_CR2","doi-asserted-by":"crossref","unstructured":"Banerjee, A., Naumann, D.A., Rosenberg, S.: Regional Logic for Local Reasoning about Global Invariants. In: Proceedings of ECOOP\u201908, pp 387\u2013411. Springer (2008)","DOI":"10.1007\/978-3-540-70592-5_17"},{"key":"9531_CR3","unstructured":"Barrett, C., Sebastiani, R., Seshia, S.A., Tinelli, C.: Handbook of Satisfiability, chap. Satisfiability Modulo Theories. IOS Press (2008)"},{"key":"9531_CR4","doi-asserted-by":"crossref","unstructured":"Baukus, K., Bensalem, S., Lakhnech, Y., Stahl, K.: Abstracting WS1S Systems to Verify Parameterized Networks. In: Proceedings of TACAS\u201900, LNCS, vol. 1785, pp 188\u2013203. Springer (2000)","DOI":"10.1007\/3-540-46419-0_14"},{"key":"9531_CR5","doi-asserted-by":"crossref","unstructured":"Baukus, K., Lakhnech, Y., Stahl, K.: Verifying Universal Properties of Parameterized Networks. In: Proceedings of FTRTFT\u201900, LNCS, vol. 1926, pp 291\u2013303. Springer (2000)","DOI":"10.1007\/3-540-45352-0_24"},{"key":"9531_CR6","doi-asserted-by":"crossref","unstructured":"Baukus, K., Lakhnech, Y., Stahl, K.: Parameterized Verification of a Cache Coherence Protocol: Safety and Liveness. In: Proceedings of VMCAI\u201902, LNCS, vol. 2294, pp 317\u2013330. Springer (2002)","DOI":"10.1007\/3-540-47813-2_22"},{"key":"9531_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 (2008)","DOI":"10.1007\/978-3-540-70545-1_37"},{"issue":"3","key":"9531_CR8","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1023\/A:1008700623084","volume":"16","author":"N Bj\u00f8rner","year":"2000","unstructured":"Bj\u00f8rner, N., Browne, A., Col\u00f3n, M., Finkbeiner, B., Manna, Z., Sipma, H., Uribe, T.E.: Verifying temporal properties of reactive systems: A STeP tutorial. Form. Meth. in Sys. Design 16(3), 227\u2013270 (2000)","journal-title":"Form. Meth. in Sys. Design"},{"key":"9531_CR9","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Dragoi, C., Enea, C., Sighireanu, M.: A Logic-Based Framework for Reasoning about Composite Data Structures. In: Proceedings of CONCUR\u201909, pp 178\u2013195. Springer (2009)","DOI":"10.1007\/978-3-642-04081-8_13"},{"key":"9531_CR10","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 (2006)","DOI":"10.1007\/11609773_28"},{"key":"9531_CR11","doi-asserted-by":"crossref","unstructured":"Brookes, S.D.: A Semantics for Concurrent Separation Logic. In: Proceedings of CONCUR\u201904, LNCS, vol. 3170, pp 16\u201334. Springer (2004)","DOI":"10.1007\/978-3-540-28644-8_2"},{"key":"9531_CR12","doi-asserted-by":"crossref","unstructured":"Browne, A., Manna, Z., Sipma, H.B.: Generalized Temporal Verification Diagrams. In: Proceedings of FSTTCS\u201995, LNCS, vol. 1206, pp 484\u2013498. Springer (1995)","DOI":"10.1007\/3-540-60692-0_69"},{"key":"9531_CR13","doi-asserted-by":"crossref","unstructured":"Bultan, T., Gerber, R., Pugh, W.: Symbolic Model Checking of Infinite State Systems Using Presburger Arithmetic. In: Proceedings of CAV\u201997, LNCS, vol. 1254, pp 400\u2013411. Springer (1997)","DOI":"10.1007\/3-540-63166-6_39"},{"key":"9531_CR14","doi-asserted-by":"crossref","unstructured":"Cern\u00fd, P., Radhakrishna, A., Zufferey, D., Chaudhuri, S., Alur, R.: Model Checking of Linearizability of Concurrent List Implementations. In: Proceedings of CAV\u201910, LNCS, vol. 6174, pp 465\u2013479. Springer (2010)","DOI":"10.1007\/978-3-642-14295-6_41"},{"key":"9531_CR15","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 (1987)","DOI":"10.1145\/41840.41865"},{"key":"9531_CR16","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., Browne, M.C.: Reasoning about Networks with Many Identical Finite-State Processes. In: Proceedings of PODC\u201986, pp 240\u2013248. ACM (1986)","DOI":"10.1145\/10590.10611"},{"key":"9531_CR17","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 (2008)","DOI":"10.1007\/978-3-540-78800-3_4"},{"key":"9531_CR18","doi-asserted-by":"crossref","unstructured":"Cook, B., Gotsman, A., Podelski, A., Rybalchenko, A., Vardi, M.Y.: Proving that Programs Eventually Do Something Good. In: Proceedings of POPL\u201907, pp 265\u2013276. ACM (2007)","DOI":"10.1145\/1190216.1190257"},{"issue":"1\/2","key":"9531_CR19","first-page":"117","volume":"12","author":"N Dershowitz","year":"2001","unstructured":"Dershowitz, N., Lindenstrauss, N., Sagiv, Y., Serebrenik, A.: A general framework for automatic termination analysis of logic programs. Applicable Algebra in Engineering. Communication and Computing 12(1\/2), 117\u2013156 (2001)","journal-title":"Communication and Computing"},{"key":"9531_CR20","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 (2000)","DOI":"10.1007\/10721959_19"},{"key":"9531_CR21","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Kahlon, V.: Model Checking Large-Scale and Parameterized Resource Allocation Systems. In: TACAS, LNCS, vol. 2280, pp 251\u2013265. Springer (2002)","DOI":"10.1007\/3-540-46002-0_18"},{"key":"9531_CR22","doi-asserted-by":"crossref","unstructured":"Farzan, A., Kincaid, Z.: Verification of Parameterized Concurrent Programs by Modular Reasoning about Data and Control. In: Proceedings of POPL\u201912, pp 297\u2013308. ACM (2012)","DOI":"10.1145\/2103656.2103693"},{"key":"9531_CR23","doi-asserted-by":"crossref","unstructured":"Giesl, J., Brockschmidt, M., Emmes, F., Frohn, F., Fuhs, C., Otto, C., Pl\u00fccker, M., Schneider-kamp, P., Str\u00f6der, T., Swiderski, S., Thiemann, R.: Proving Termination of Programs Automatically with AProVE. In: Proceedings of IJCAR\u201914, LNCS, vol. 8562, pp 184\u2013191. Springer (2014)","DOI":"10.1007\/978-3-319-08587-6_13"},{"key":"9531_CR24","doi-asserted-by":"crossref","unstructured":"Goel, A., Krstic, S., Leslie, R., Tuttle, M.R.: SMT-Based System Verification with DVF. In: Proceedings of SMT\u201912, Easychair, EPiC Series, vol. 20, pp 32\u201343 (2012)","DOI":"10.29007\/59rn"},{"key":"9531_CR25","doi-asserted-by":"crossref","unstructured":"Gotsman, A., Cook, B., Parkinson, M.J., Vafeiadis, V.: Proving that Non-Blocking Algorithms Don\u2019t Block. In: Shao, Z., Pierce, B.C. (eds.) Proceedings of POPL\u201909, pp 16\u201328. ACM (2009)","DOI":"10.1145\/1594834.1480886"},{"key":"9531_CR26","unstructured":"Groves, L.: Verifying Michael and Scott\u2019s Lock-Free Queue Algorithm Using Trace Reduction. In: CATS, CRPIT, vol. 77, pp 133\u2013142. Australian Computer Society (2008)"},{"key":"9531_CR27","unstructured":"Herlihy, M., Shavit, N.: The art of multiprocessor programming. Morgan-Kaufmann (2008)"},{"key":"9531_CR28","doi-asserted-by":"crossref","unstructured":"Hobor, A., Appel, A.W., Nardelli, F.Z.: Oracle Semantics for Concurrent Separation Logic. In: Proceedings of ESOP\u201908, LNCS, vol. 4960, pp 353\u2013367. Springer (2008)","DOI":"10.1007\/978-3-540-78739-6_27"},{"issue":"7","key":"9531_CR29","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1145\/360248.360251","volume":"19","author":"RM Keller","year":"1976","unstructured":"Keller, R.M.: Formal verification of parallel programs. Commun. ACM 19(7), 371\u2013384 (1976)","journal-title":"Commun. ACM"},{"key":"9531_CR30","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 (2008)","DOI":"10.1145\/1328438.1328461"},{"issue":"8","key":"9531_CR31","doi-asserted-by":"crossref","first-page":"453","DOI":"10.1145\/361082.361093","volume":"17","author":"L Lamport","year":"1974","unstructured":"Lamport, L.: A new solution of Dijkstra\u2019s concurrent programming problem. Commun. ACM 17(8), 453\u2013455 (1974)","journal-title":"Commun. ACM"},{"key":"9531_CR32","doi-asserted-by":"crossref","unstructured":"Manna, Z., Browne, A., Sipma, H., Uribe, T.E.: Visual Abstractions for Temporal Verification. In: Proceedings of AMAST\u201998, LNCS, vol. 1548, pp 28\u201341. Springer (1998)","DOI":"10.1007\/3-540-49253-4_5"},{"key":"9531_CR33","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: Temporal verification of reactive systems: Safety. springer (1995)","DOI":"10.1007\/978-1-4612-4222-2"},{"key":"9531_CR34","doi-asserted-by":"crossref","unstructured":"Manna, Z., Sipma, H.: Verification of Parameterized Systems by Dynamic Induction on Diagrams. In: Proceedings of CAV\u201999, LNCS, vol. 1633. Springer (1999)","DOI":"10.1007\/3-540-48683-6_5"},{"key":"9531_CR35","doi-asserted-by":"crossref","unstructured":"Marco Bozzano, G.D.: Beyond Parameterized Verification. In: Proceedings of TACAS\u201902, LNCS, vol. 2280, pp 221\u2013235. Springer (2002)","DOI":"10.1007\/3-540-46002-0_16"},{"key":"9531_CR36","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1016\/0304-3975(84)90049-5","volume":"32","author":"S Miyano","year":"1984","unstructured":"Miyano, S., Hayashi, T.: Alternating finite automata on \u03c9-words. Theor. Comput. Sci. 32, 321\u2013330 (1984)","journal-title":"Theor. Comput. Sci."},{"key":"9531_CR37","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P.W.: Resources, Concurrency and Local Reasoning. In: Proceedings of CONCUR\u201904, LNCS, vol. 3170, pp 49\u201367. Springer (2004)","DOI":"10.1007\/978-3-540-28644-8_4"},{"key":"9531_CR38","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P.W., Reynolds, J.C., Yang, H.: Local Reasoning about Programs that Alter Data Structures. In: Proceedings of CSL\u201901, LNCS, vol. 2142, pp 1\u201319. Springer (2001)","DOI":"10.1007\/3-540-44802-0_1"},{"key":"9531_CR39","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The Temporal Logic of Programs. In: Proceedings of FOCS\u201977, pp 46\u201357. IEEE Computer Society Press (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"9531_CR40","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Shahar, E.: Liveness and Acceleration in Parameterized Verification. In: Proceedings of CAV\u201900, vol. 1855, pp 328\u2013343. Springer (2000)","DOI":"10.1007\/10722167_26"},{"key":"9531_CR41","doi-asserted-by":"crossref","unstructured":"Podelsky, A., Rybalchenko, A.: Transition Invariants. In: Proceedings of LICS\u201904, pp 32\u201341. IEEE Computer Society Press (2004)","DOI":"10.1109\/LICS.2004.1319598"},{"key":"9531_CR42","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation Logic: a Logic for Shared Mutable Data Structures. In: Proceedings of LICS\u201902, pp 55\u201374. IEEE Computer Society Press (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"9531_CR43","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 (2010)","DOI":"10.1007\/978-3-642-16901-4_7"},{"key":"9531_CR44","doi-asserted-by":"crossref","unstructured":"S\u00e1nchez, A., S\u00e1nchez, C.: A Theory of Skiplists with Applications to the Verification of Concurrent Datatypes. In: Proceedings of NFM\u201911, LNCS, vol. 6617, pp 343\u2013358. Springer (2011)","DOI":"10.1007\/978-3-642-20398-5_25"},{"key":"9531_CR45","doi-asserted-by":"crossref","unstructured":"S\u00e1nchez, A., S\u00e1nchez, C.: Formal Verification of Skiplists with Arbitrary Many Levels. In: Proceedings of ATVA\u201914, vol. 8837, pp 314\u2013329. Springer (2014)","DOI":"10.1007\/978-3-319-11936-6_23"},{"key":"9531_CR46","doi-asserted-by":"crossref","unstructured":"S\u00e1nchez, A., S\u00e1nchez, C.: LEAP: A Tool for the Parametrized Verification of Concurrent Datatypes. In: Proceedings of CAV\u201914, vol. 8559, pp 620\u2013627. Springer (2014)","DOI":"10.1007\/978-3-319-08867-9_41"},{"key":"9531_CR47","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 (2014)","DOI":"10.1109\/TIME.2014.11"},{"issue":"6","key":"9531_CR48","doi-asserted-by":"crossref","first-page":"525","DOI":"10.1007\/s00236-015-0222-5","volume":"52","author":"A S\u00e1nchez","year":"2015","unstructured":"S\u00e1nchez, A., S\u00e1nchez, C.: Parametrized invariance for infinite state processes. Acta Inf. 52(6), 525\u2013557 (2015)","journal-title":"Acta Inf."},{"key":"9531_CR49","doi-asserted-by":"crossref","unstructured":"Sethi, D., Talupur, M., Schwartz-Narbonne, D., Malik, S.: Parameterized Model Checking of Fine Grained Concurrency. In: Proceedings of SPIN\u201912, pp 208\u2013226. Springer (2012)","DOI":"10.1007\/978-3-642-31759-0_15"},{"key":"9531_CR50","unstructured":"Sipma, H.B.: Diagram-Based Verification of Discrete, Real-Time and Hybrid Systems. Ph.D. thesis, Stanford University (1999)"},{"key":"9531_CR51","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. Proc. Letters 28, 213\u2013214 (1988)","journal-title":"Inf. Proc. Letters"},{"key":"9531_CR52","doi-asserted-by":"crossref","unstructured":"Vafeiadis, V., Herlihy, M., Hoare, T., Shapiro, M.: Proving Correctness of Highly-Concurrent Linearisable Objects. In: Proceedings of PPOPP\u201906, pp 129\u2013136. ACM (2006)","DOI":"10.1145\/1122971.1122992"},{"key":"9531_CR53","doi-asserted-by":"crossref","unstructured":"Vechev, M.T., Yahav, E., Yorsh, G.: Experience with Model Checking Linearizability. In: Proceedings of SPIN\u201909, LNCS, vol. 5578, pp 261\u2013278. Springer (2009)","DOI":"10.1007\/978-3-642-02652-2_21"},{"key":"9531_CR54","doi-asserted-by":"crossref","unstructured":"Wies, T., Piskac, R., Kuncak, V.: Combining Theories with Shared Set Operations. In: Proceedings of FROCOS\u201909, LNCS, vol. 5749, pp 366\u2013382. Springer (2009)","DOI":"10.1007\/978-3-642-04222-5_23"},{"key":"9531_CR55","doi-asserted-by":"crossref","unstructured":"Yorsh, G., Rabinovich, A.M., Sagiv, M., Meyer, A., Bouajjani, A.: A Logic of Reachable Patterns in Linked Data-Structures. In: Proceedings of FOSSACS\u201906, pp 94\u2013110 (2006)","DOI":"10.1007\/11690634_7"},{"issue":"1-2","key":"9531_CR56","doi-asserted-by":"crossref","first-page":"111","DOI":"10.1016\/j.jlap.2006.12.001","volume":"73","author":"G Yorsh","year":"2007","unstructured":"Yorsh, G., Rabinovich, A.M., Sagiv, M., Meyer, A., Bouajjani, A.: A logic of reachable patterns in linked data-structures. J. Log. Algebr. Program. 73(1-2), 111\u2013142 (2007)","journal-title":"J. Log. Algebr. Program."},{"key":"9531_CR57","doi-asserted-by":"crossref","unstructured":"Zhang, S.J.: Scalable Automatic Linearizability Checking. In: Proceedings of ICSE\u201911, vol. 5578, pp 1185\u20131187. ACM (2011)","DOI":"10.1145\/1985793.1986037"}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10472-016-9531-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-016-9531-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-016-9531-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,12]],"date-time":"2025-06-12T17:57:05Z","timestamp":1749751025000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10472-016-9531-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,11,15]]},"references-count":57,"journal-issue":{"issue":"3-4","published-print":{"date-parts":[[2017,8]]}},"alternative-id":["9531"],"URL":"https:\/\/doi.org\/10.1007\/s10472-016-9531-9","relation":{},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"type":"print","value":"1012-2443"},{"type":"electronic","value":"1573-7470"}],"subject":[],"published":{"date-parts":[[2016,11,15]]}}}