{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,25]],"date-time":"2026-02-25T17:48:35Z","timestamp":1772041715596,"version":"3.50.1"},"publisher-location":"Cham","reference-count":14,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031606977","type":"print"},{"value":"9783031606984","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"DOI":"10.1007\/978-3-031-60698-4_7","type":"book-chapter","created":{"date-parts":[[2024,5,27]],"date-time":"2024-05-27T00:01:51Z","timestamp":1716768111000},"page":"118-135","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Verification of\u00a0Scapegoat Trees Using Dafny"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0002-2194-0029","authenticated-orcid":false,"given":"Jiapeng","family":"Wang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3923-7972","authenticated-orcid":false,"given":"Sini","family":"Chen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0214-8565","authenticated-orcid":false,"given":"Huibiao","family":"Zhu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,5,26]]},"reference":[{"key":"7_CR1","doi-asserted-by":"publisher","unstructured":"Armborst, L., Huisman, M.: Permission-based verification of red-black trees and their merging. In: 2021 IEEE\/ACM 9th International Conference on Formal Methods in Software Engineering (FormaliSE), pp. 111\u2013123 (2021). https:\/\/doi.org\/10.1109\/FormaliSE52586.2021.00017","DOI":"10.1109\/FormaliSE52586.2021.00017"},{"key":"7_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/3-540-46428-X_25","volume-title":"Fundamental Approaches to Software Engineering","author":"M Balser","year":"2000","unstructured":"Balser, M., Reif, W., Schellhorn, G., Stenzel, K., Thums, A.: Formal system development with KIV. In: Maibaum, T. (ed.) FASE 2000. LNCS, vol. 1783, pp. 363\u2013366. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-46428-X_25"},{"key":"7_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/978-3-319-66845-1_7","volume-title":"Integrated Formal Methods","author":"S Blom","year":"2017","unstructured":"Blom, S., Darabi, S., Huisman, M., Oortwijn, W.: The VerCors tool set: verification of parallel and concurrent software. In: Polikarpova, N., Schneider, S. (eds.) IFM 2017. LNCS, vol. 10510, pp. 102\u2013110. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66845-1_7"},{"key":"7_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"445","DOI":"10.1007\/978-3-030-90870-6_24","volume-title":"Formal Methods","author":"F Cassez","year":"2021","unstructured":"Cassez, F.: Verification of the incremental Merkle tree algorithm with Dafny. In: Huisman, M., P\u0103s\u0103reanu, C., Zhan, N. (eds.) FM 2021. LNCS, vol. 13047, pp. 445\u2013462. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-90870-6_24"},{"key":"7_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/978-3-031-15008-1_5","volume-title":"Formal Methods for Industrial Critical Systems","author":"F Cassez","year":"2022","unstructured":"Cassez, F., Fuller, J., Quiles, H.M.A.: Deductive verification of smart contracts with Dafny. In: Groote, J.F., Huisman, M. (eds.) FMICS 2022. LNCS, vol. 13487, pp. 50\u201366. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-15008-1_5"},{"key":"7_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-319-12154-3_11","volume-title":"Verified Software: Theories, Tools and Experiments","author":"M Clochard","year":"2014","unstructured":"Clochard, M.: Automatically verified implementation of data structures based on AVL trees. In: Giannakopoulou, D., Kroening, D. (eds.) VSTTE 2014. LNCS, vol. 8471, pp. 167\u2013180. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-12154-3_11"},{"key":"7_CR7","doi-asserted-by":"publisher","unstructured":"Galperin, I., Rivest, R.L.: Scapegoat trees. In: Proceedings of the Fourth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 1993, pp. 165\u2013174. Society for Industrial and Applied Mathematics, USA (1993). https:\/\/doi.org\/10.5555\/313559.313676","DOI":"10.5555\/313559.313676"},{"issue":"10","key":"7_CR8","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580 (1969). https:\/\/doi.org\/10.1145\/363235.363259","journal-title":"Commun. ACM"},{"key":"7_CR9","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-17511-4_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"KRM Leino","year":"2010","unstructured":"Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348\u2013370. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20"},{"key":"7_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/978-3-319-71237-6_13","volume-title":"Programming Languages and Systems","author":"T Nipkow","year":"2017","unstructured":"Nipkow, T.: Verified root-balanced trees. In: Chang, B.-Y.E. (ed.) APLAS 2017. LNCS, vol. 10695, pp. 255\u2013272. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-71237-6_13"},{"issue":"4","key":"7_CR11","doi-asserted-by":"publisher","first-page":"767","DOI":"10.1007\/s10817-019-09534-y","volume":"64","author":"R Pe\u00f1a","year":"2020","unstructured":"Pe\u00f1a, R.: An assertional proof of red-black trees using Dafny. J. Autom. Reason. 64(4), 767\u2013791 (2020). https:\/\/doi.org\/10.1007\/s10817-019-09534-y","journal-title":"J. Autom. Reason."},{"key":"7_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/978-3-031-25803-9_8","volume-title":"Verified Software. Theories, Tools and Experiments","author":"G Schellhorn","year":"2022","unstructured":"Schellhorn, G., Bodenm\u00fcller, S., Bitterlich, M., Reif, W.: Separating separation logic-modular verification of red-black trees. In: Lal, A., Tonetta, S. (eds.) VSTTE 2022. LNCS, vol. 13800, pp. 129\u2013147. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-25803-9_8"},{"key":"7_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/978-3-319-43144-4_27","volume-title":"Interactive Theorem Proving","author":"B Zhan","year":"2016","unstructured":"Zhan, B.: AUTO2, a saturation-based heuristic prover for higher-order logic. In: Blanchette, J.C., Merz, S. (eds.) ITP 2016. LNCS, vol. 9807, pp. 441\u2013456. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-43144-4_27"},{"key":"7_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-319-89960-2_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"B Zhan","year":"2018","unstructured":"Zhan, B.: Efficient verification of imperative programs using Auto2. In: Beyer, D., Huisman, M. (eds.) TACAS 2018, Part I. LNCS, vol. 10805, pp. 23\u201340. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89960-2_2"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-60698-4_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,5,27]],"date-time":"2024-05-27T00:02:39Z","timestamp":1716768159000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-60698-4_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031606977","9783031606984"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-60698-4_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"26 May 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"NFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"NASA Formal Methods Symposium","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Moffett Field, CA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 June 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 June 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"nfm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}