{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,30]],"date-time":"2026-04-30T18:45:30Z","timestamp":1777574730368,"version":"3.51.4"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319088662","type":"print"},{"value":"9783319088679","type":"electronic"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-08867-9_41","type":"book-chapter","created":{"date-parts":[[2014,6,28]],"date-time":"2014-06-28T07:37:30Z","timestamp":1403941050000},"page":"620-627","source":"Crossref","is-referenced-by-count":6,"title":["LEAP: A Tool for the Parametrized Verification of Concurrent Datatypes"],"prefix":"10.1007","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","reference":[{"key":"41_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/3-540-48683-6_14","volume-title":"Computer Aided Verification","author":"P.A. Abdulla","year":"1999","unstructured":"Abdulla, P.A., Bouajjani, A., Jonsson, B., Nilsson, M.: Handling global conditions in parametrized system verification. In: Halbwachs, N., Peled, D. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 134\u2013145. Springer, Heidelberg (1999)"},{"issue":"2","key":"41_CR2","first-page":"126","volume":"34","author":"P.A. Abdulla","year":"2009","unstructured":"Abdulla, P.A., Delzanno, G., Rezine, A.: Approximated parameterized verif. of infinite-state processes with global conditions. FMSD\u00a034(2), 126\u2013156 (2009)","journal-title":"FMSD"},{"issue":"6","key":"41_CR3","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1016\/0020-0190(86)90071-2","volume":"22","author":"K.R. Apt","year":"1986","unstructured":"Apt, K.R., Kozen, D.C.: Limits for automatic verification of finite-state concurrent systems. Information Processing Letters\u00a022(6), 307\u2013309 (1986)","journal-title":"Information Processing Letters"},{"key":"41_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/11804192_6","volume-title":"Formal Methods for Components and Objects","author":"J. Berdine","year":"2006","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: Smallfoot: Modular automatic assertion checking with separation logic. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol.\u00a04111, pp. 115\u2013137. Springer, Heidelberg (2006)"},{"key":"41_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/11609773_28","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A.R. Bradley","year":"2006","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: What\u2019s decidable about arrays? In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol.\u00a03855, pp. 427\u2013442. Springer, Heidelberg (2006)"},{"key":"41_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"484","DOI":"10.1007\/3-540-60692-0_69","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"I.A. Browne","year":"1995","unstructured":"Browne, I.A., Manna, Z., Sipma, H.B.: Generalized verification diagrams. In: Thiagarajan, P.S. (ed.) FSTTCS 1995. LNCS, vol.\u00a01026, pp. 484\u2013498. Springer, Heidelberg (1995)"},{"key":"41_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1007\/978-3-642-14808-8_3","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2010","author":"K. Chaudhuri","year":"2010","unstructured":"Chaudhuri, K., Doligez, D., Lamport, L., Merz, S.: The TLA\u2009+\u2009 proof system: Building a heterogeneous verification platform. In: Cavalcanti, A., Deharbe, D., Gaudel, M.-C., Woodcock, J. (eds.) ICTAC 2010. LNCS, vol.\u00a06255, p. 44. Springer, Heidelberg (2010)"},{"key":"41_CR8","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O.: Avoiding the state explosion problem in temporal logic model checking. In: Proc. of PODC 1987, pp. 294\u2013303. ACM (1987)","DOI":"10.1145\/41840.41865"},{"key":"41_CR9","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., Browne, M.C.: Reasoning about networks with many identical finite-state procs. In: Proc. of PODC 1986, pp. 240\u2013248. ACM (1986)","DOI":"10.1145\/10590.10611"},{"key":"41_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-642-03359-9_2","volume-title":"Theorem Proving in Higher Order Logics","author":"E. Cohen","year":"2009","unstructured":"Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: A practical system for verifying concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 23\u201342. Springer, Heidelberg (2009)"},{"key":"41_CR11","doi-asserted-by":"crossref","unstructured":"Condit, J., Hackett, B., Lahiri, S.K., Qadeer, S.: Unifying type checking and property checking for low-level code. In: Proc. of POPL 2009, pp. 302\u2013314. ACM Press (2009)","DOI":"10.1145\/1594834.1480921"},{"key":"41_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-642-33826-7_16","volume-title":"Software Engineering and Formal Methods","author":"P. Cuoq","year":"2012","unstructured":"Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C \u2013 a software analysis perspective. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM 2012. LNCS, vol.\u00a07504, pp. 233\u2013247. Springer, Heidelberg (2012)"},{"key":"41_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"41_CR14","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Kahlon, V.: Reducing model checking of the many to the few. In: McAllester, D. (ed.) CADE-17. LNCS (LNAI), vol.\u00a01831, pp. 236\u2013254. Springer, Heidelberg (2000)","DOI":"10.1007\/10721959_19"},{"key":"41_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/978-3-540-27813-9_14","volume-title":"Computer Aided Verification","author":"H. Ganzinger","year":"2004","unstructured":"Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): Fast decision procedures. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 175\u2013188. Springer, Heidelberg (2004)"},{"key":"41_CR16","unstructured":"Herlihy, M., Shavit, N.: The Art of Multiprocessor Programming. Morgan- Kaufmann (2008)"},{"key":"41_CR17","doi-asserted-by":"crossref","unstructured":"Kuncak, V., Rinard, M.C.: An overview of the Jahob analysis system: Project goals and current status. In: Proc. of IPDPS 2006. IEEE Computer Society Press (2006)","DOI":"10.1109\/IPDPS.2006.1639580"},{"key":"41_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-642-11319-2_2","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"K.R.M. Leino","year":"2010","unstructured":"Leino, K.R.M.: Verifying concurrent programs with Chalice. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol.\u00a05944, p. 2. Springer, Heidelberg (2010)"},{"key":"41_CR19","doi-asserted-by":"crossref","unstructured":"Manna, Z., Anuchitanukul, A., Bj\u00f8rner, N., Browne, A., Chang, E., Col\u00f3n, M., de Alfaro, L., Devarajan, H., Sipma, H., Uribe, T.: STeP: The stanford temporal prover. Technical Report STAN-CS-TR-94-1518, Computer Science Department, Stanford University (July 1994)","DOI":"10.21236\/ADA324036"},{"key":"41_CR20","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems. Springer (1995)","DOI":"10.1007\/978-1-4612-4222-2"},{"key":"41_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/3-540-46002-0_16","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Bozzano","year":"2002","unstructured":"Bozzano, M., Delzanno, G.: Beyond parameterized verification. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol.\u00a02280, pp. 221\u2013235. Springer, Heidelberg (2002)"},{"key":"41_CR22","doi-asserted-by":"crossref","unstructured":"Podelsky, A., Rybalchenko, A.: Transition invariants. In: Proc. of LICS 2004, pp. 32\u201341. IEEE Computer Society Press (2004)","DOI":"10.1109\/LICS.2004.1319598"},{"key":"41_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1007\/978-3-642-16901-4_7","volume-title":"Formal Methods and Software Engineering","author":"A. S\u00e1nchez","year":"2010","unstructured":"S\u00e1nchez, A., S\u00e1nchez, C.: Decision procedure for the temporal verification of concurrent lists. In: Dong, J.S., Zhu, H. (eds.) ICFEM 2010. LNCS, vol.\u00a06447, pp. 74\u201389. Springer, Heidelberg (2010)"},{"key":"41_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/978-3-642-20398-5_25","volume-title":"NASA Formal Methods","author":"A. S\u00e1nchez","year":"2011","unstructured":"S\u00e1nchez, A., S\u00e1nchez, C.: A theory of skiplists with applications to the verification of concurrent datatypes. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol.\u00a06617, pp. 343\u2013358. Springer, Heidelberg (2011)"},{"key":"41_CR25","unstructured":"S\u00e1nchez, A., S\u00e1nchez, C.: Parametrized invariance for infinite state processes. CoRR, abs\/1312.4043 (2013)"},{"key":"41_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/978-3-642-33125-1_12","volume-title":"Static Analysis","author":"A. Sanchez","year":"2012","unstructured":"Sanchez, A., Sankaranarayanan, S., S\u00e1nchez, C., Chang, B.-Y.E.: Invariant generation for parametrized systems using self-reflection. In: Min\u00e9, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol.\u00a07460, pp. 146\u2013163. Springer, Heidelberg (2012)"},{"key":"41_CR27","unstructured":"S\u00e1nchez, C., S\u00e1nchez, A.: A decidable theory of skiplists of unbounded size and arbitrary height. CoRR, abs\/1301.4372 (2013)"},{"key":"41_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1007\/978-3-540-68863-1_14","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"J. Smans","year":"2008","unstructured":"Smans, J., Jacobs, B., Piessens, F.: Vericool: An automatic verifier for a concurrent object-oriented language. In: Barthe, G., de Boer, F.S. (eds.) FMOODS 2008. LNCS, vol.\u00a05051, pp. 220\u2013239. Springer, Heidelberg (2008)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-08867-9_41","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T22:37:53Z","timestamp":1558305473000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-08867-9_41"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319088662","9783319088679"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-08867-9_41","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}