{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,11,12]],"date-time":"2026-11-12T12:41:30Z","timestamp":1794487290352,"version":"4.9.1"},"publisher-location":"Cham","reference-count":20,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319119359","type":"print"},{"value":"9783319119366","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-11936-6_23","type":"book-chapter","created":{"date-parts":[[2014,10,24]],"date-time":"2014-10-24T15:11:50Z","timestamp":1414163510000},"page":"314-329","source":"Crossref","is-referenced-by-count":2,"title":["Formal Verification of Skiplists with Arbitrary Many Levels"],"prefix":"10.1007","author":[{"given":"Alejandro","family":"S\u00e1nchez","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"C\u00e9sar","family":"S\u00e1nchez","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"23_CR1","unstructured":"The KDE Platform, http:\/\/kde.org\/"},{"key":"23_CR2","unstructured":"KDE Skiplist implementation, http:\/\/api.kde.org\/4.1-api\/kdeedu-apidocs\/kstars\/html\/SkipList_8cpp_source.html"},{"key":"23_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"224","DOI":"10.1007\/978-3-319-02444-8_17","volume-title":"Automated Technology for Verification and Analysis","author":"P.A. Abdulla","year":"2013","unstructured":"Abdulla, P.A., Hol\u00edk, L., Jonsson, B., Leng\u00e1l, O., Trinh, C.Q., Vojnar, T.: Verification of heap manipulating programs with ordered data by extended forest automata. In: Van Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol.\u00a08172, pp. 224\u2013239. Springer, Heidelberg (2013)"},{"key":"23_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/978-3-642-04081-8_13","volume-title":"CONCUR 2009 - Concurrency Theory","author":"A. Bouajjani","year":"2009","unstructured":"Bouajjani, A., Dr\u0103goi, C., Enea, C., Sighireanu, M.: A logic-based framework for reasoning about composite data structures. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol.\u00a05710, pp. 178\u2013195. Springer, Heidelberg (2009)"},{"key":"23_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":"23_CR6","unstructured":"Gallier, J.H.: Logic for Computer Science: Foundations of Automatic Theorem Proving. Harper & Row (1986)"},{"key":"23_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"740","DOI":"10.1007\/978-3-642-39799-8_52","volume-title":"Computer Aided Verification","author":"L. Hol\u00edk","year":"2013","unstructured":"Hol\u00edk, L., Leng\u00e1l, O., Rogalewicz, A., \u0160im\u00e1\u010dek, J., Vojnar, T.: Fully automated shape analysis based on forest automata. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol.\u00a08044, pp. 740\u2013755. Springer, Heidelberg (2013)"},{"key":"23_CR8","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/11532231_20","volume-title":"Automated Deduction \u2013 CADE-20","author":"V. Kuncak","year":"2005","unstructured":"Kuncak, V., Nguyen, H.H., Rinard, M.C.: An algorithm for deciding BAPA: Boolean Algebra with Presburger Arithmetic. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol.\u00a03632, pp. 260\u2013277. Springer, Heidelberg (2005)"},{"key":"23_CR9","doi-asserted-by":"crossref","unstructured":"Lahiri, S.K., Qadeer, S.: Back to the future: revisiting precise program verification using SMT solvers. In: Proc. of POPL 2008, pp. 171\u2013182. ACM (2008)","DOI":"10.1145\/1328897.1328461"},{"key":"23_CR10","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: Temporal Verif. of Reactive Systems. Springer (1995)","DOI":"10.1007\/978-1-4612-4222-2"},{"key":"23_CR11","unstructured":"McCarthy, J.: Towards a mathematical science of computation. In: IFIP Congress, pp. 21\u201328 (1962)"},{"issue":"2","key":"23_CR12","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G. Nelson","year":"1979","unstructured":"Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst.\u00a01(2), 245\u2013257 (1979)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"6","key":"23_CR13","doi-asserted-by":"publisher","first-page":"668","DOI":"10.1145\/78973.78977","volume":"33","author":"W. Pugh","year":"1990","unstructured":"Pugh, W.: Skip lists: A probabilistic alternative to balanced trees. Commun. ACM\u00a033(6), 668\u2013676 (1990)","journal-title":"Commun. ACM"},{"key":"23_CR14","unstructured":"Ranise, S., Zarba, C.G.: A theory of singly-linked lists and its extensible decision procedure. In: Proc. of SEFM 2006. IEEE CS Press (2006)"},{"key":"23_CR15","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Proc. of LICS 2002, pp. 55\u201374. IEEE CS Press (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"23_CR16","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 procedures 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":"23_CR17","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":"23_CR18","unstructured":"S\u00e1nchez, A., S\u00e1nchez, C.: Parametrized invariance for infinite state processes. CoRR, abs\/1312.4043 (2013)"},{"key":"23_CR19","unstructured":"Wies, T., Kuncak, V., Zee, K., Podelski, A., Rinard, M.: Verifying complex properties using symbolic shape analysis. In: Workshop on Heap Abstraction and Verification (collocated with ETAPS) (2007)"},{"key":"23_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1007\/11690634_7","volume-title":"Foundations of Software Science and Computation Structures","author":"G. Yorsh","year":"2006","unstructured":"Yorsh, G., Rabinovich, A.M., Sagiv, M., Meyer, A., Bouajjani, A.: A logic of reachable patterns in linked data-structures. In: Aceto, L., Ing\u00f3lfsd\u00f3ttir, A. (eds.) FOSSACS 2006. LNCS, vol.\u00a03921, pp. 94\u2013110. Springer, Heidelberg (2006)"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-11936-6_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,5]],"date-time":"2025-05-05T09:08:48Z","timestamp":1746436128000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-11936-6_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319119359","9783319119366"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-11936-6_23","relation":{"is-part-of":[{"id-type":"doi","id":"https:\/\/doi.org\/10.1007\/978-3-319-11936-6","asserted-by":"object"}]},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}