{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:39:22Z","timestamp":1780994362711,"version":"3.54.1"},"publisher-location":"Cham","reference-count":37,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031572456","type":"print"},{"value":"9783031572463","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:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,4,4]],"date-time":"2024-04-04T00:00:00Z","timestamp":1712188800000},"content-version":"vor","delay-in-days":94,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>In this experience report, we present the complete formal verification of a Java implementation of inplace superscalar sample sort (\n\"Image missing\") using the KeY program verification system. As \n\"Image missing\" is one of the fastest general purpose sorting algorithms, this is an important step towards a collection of basic toolbox components that are both provably correct and highly efficient. At the same time, it is an important case study of how careful, highly efficient implementations of complicated algorithms can be formally verified directly. We provide an analysis of which features of the KeY system and its verification calculus are instrumental in enabling algorithm verification without any compromise on algorithm efficiency.<\/jats:p>","DOI":"10.1007\/978-3-031-57246-3_15","type":"book-chapter","created":{"date-parts":[[2024,4,3]],"date-time":"2024-04-03T14:03:43Z","timestamp":1712153023000},"page":"268-287","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Formally Verifying an Efficient Sorter"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9672-3291","authenticated-orcid":false,"given":"Bernhard","family":"Beckert","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3330-9349","authenticated-orcid":false,"given":"Peter","family":"Sanders","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2350-1831","authenticated-orcid":false,"given":"Mattias","family":"Ulbrich","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Julian","family":"Wiesler","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7867-3200","authenticated-orcid":false,"given":"Sascha","family":"Witt","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2024,4,4]]},"reference":[{"key":"15_CR1","doi-asserted-by":"publisher","unstructured":"Ahrendt, W., Beckert, B., Bubel, R., H\u00e4hnle, R., Schmitt, P.H., Ulbrich, M. (eds.): Deductive Software Verification - The KeY Book - From Theory to Practice, Lecture Notes in Computer Science, vol. 10001. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-49812-6","DOI":"10.1007\/978-3-319-49812-6"},{"key":"15_CR2","doi-asserted-by":"crossref","unstructured":"Axtmann, M., Ferizovic, D., Sanders, P., Witt, S.: Engineering in-place (shared-memory) sorting algorithms. ACM Transaction on Parallel Computing 9(1), 2:1\u20132:62 (2022), see also github.com\/ips4o. Conference version in ESA 2017","DOI":"10.1145\/3505286"},{"key":"15_CR3","doi-asserted-by":"publisher","unstructured":"Beckert, B., Sanders, P., Ulbrich, M., Wiesler, J., Witt, S.: Formally verifying an efficient sorter, extended version. Tech. rep., Karlsruhe Institute of Technology (2024). https:\/\/doi.org\/10.5445\/IR\/1000167846","DOI":"10.5445\/IR\/1000167846"},{"key":"15_CR4","doi-asserted-by":"crossref","unstructured":"Beckert, B., Schiffl, J., Schmitt, P.H., Ulbrich, M.: Proving JDK\u2019s dual pivot quicksort correct. In: Working Conference on Verified Software: Theories, Tools, and Experiments. pp. 35\u201348. Springer (2017)","DOI":"10.1007\/978-3-319-72308-2_3"},{"key":"15_CR5","doi-asserted-by":"crossref","unstructured":"Boer, M.d., Gouw, S.d., Klamroth, J., Jung, C., Ulbrich, M., Weigl, A.: Formal specification and verification of JDK\u2019s identity hash map implementation. In: International Conference on Integrated Formal Methods. pp. 45\u201362.Springer (2022)","DOI":"10.1007\/978-3-031-07727-2_4"},{"key":"15_CR6","doi-asserted-by":"publisher","unstructured":"Bottesch, R., Haslbeck, M.W., Thiemann, R.: A verified efficient implementation of the LLL basis reduction algorithm. In: LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Awassa, Ethiopia, 16-21 November 2018. pp. 164\u2013180 (2018). https:\/\/doi.org\/10.29007\/xwwh","DOI":"10.29007\/xwwh"},{"key":"15_CR7","doi-asserted-by":"publisher","unstructured":"Broy, M., Pepper, P.: Combining algebraic and algorithmic reasoning: An approach to the schorr-waite algorithm. ACM Trans. Program. Lang. Syst. 4(3), 362\u2013381 (1982). https:\/\/doi.org\/10.1145\/357172.357175","DOI":"10.1145\/357172.357175"},{"key":"15_CR8","doi-asserted-by":"publisher","unstructured":"Bubel, R.: The Schorr-Waite-algorithm. In: Verification of Object-Oriented Software. The KeY Approach - Foreword by K. Rustan M. Leino, pp. 569\u2013587 (2007). https:\/\/doi.org\/10.1007\/978-3-540-69061-0_15","DOI":"10.1007\/978-3-540-69061-0_15"},{"key":"15_CR9","doi-asserted-by":"publisher","unstructured":"Filli\u00e2tre, J., Paskevich, A.: Why3 - where programs meet provers. In: Programming Languages and Systems - 22nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings. pp. 125\u2013128 (2013). https:\/\/doi.org\/10.1007\/978-3-642-37036-6_8","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"15_CR10","doi-asserted-by":"crossref","unstructured":"Frazer, W.D., McKellar, A.C.: Samplesort: A sampling approach to minimal storage tree sorting. Journal of the ACM (JACM) 17(3), 496\u2013507 (1970)","DOI":"10.1145\/321592.321600"},{"key":"15_CR11","doi-asserted-by":"crossref","unstructured":"de\u00a0Gouw, S., de\u00a0Boer, F.S., Bubel, R., H\u00e4hnle, R., Rot, J., Steinh\u00f6fel, D.: Verifying OpenJDK\u2019s sort method for generic collections. Journal of Automated Reasoning 62(1), 93\u2013126 (2019)","DOI":"10.1007\/s10817-017-9426-4"},{"key":"15_CR12","doi-asserted-by":"publisher","unstructured":"de\u00a0Gouw, S., de\u00a0Boer, F.S., Rot, J.: Verification of counting sort and radix sort. In: Deductive Software Verification - The KeY Book - From Theory to Practice, pp. 609\u2013618 (2016). https:\/\/doi.org\/10.1007\/978-3-319-49812-6_19","DOI":"10.1007\/978-3-319-49812-6_19"},{"key":"15_CR13","doi-asserted-by":"crossref","unstructured":"Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press (2000)","DOI":"10.7551\/mitpress\/2516.001.0001"},{"key":"15_CR14","doi-asserted-by":"publisher","unstructured":"Haslbeck, M.P.L., Lammich, P.: For a few dollars more: Verified fine-grained algorithm analysis down to LLVM. ACM Trans. Program. Lang. Syst. 44(3), 14:1\u201314:36 (2022). https:\/\/doi.org\/10.1145\/3486169","DOI":"10.1145\/3486169"},{"key":"15_CR15","doi-asserted-by":"publisher","unstructured":"Hatcliff, J., Leavens, G.T., Leino, K.R.M., M\u00fcller, P., Parkinson, M.J.: Behavioral interface specification languages. ACM Comput. Surv. 44(3), 16:1\u201316:58 (2012). https:\/\/doi.org\/10.1145\/2187671.2187678","DOI":"10.1145\/2187671.2187678"},{"key":"15_CR16","doi-asserted-by":"publisher","unstructured":"Hiep, H.A., Maathuis, O., Bian, J., de\u00a0Boer, F.S., de\u00a0Gouw, S.: Verifying OpenJDK\u2019s linkedlist using key (extended paper). Int. J. Softw. Tools Technol. Transf. 24(5), 783\u2013802 (2022). https:\/\/doi.org\/10.1007\/s10009-022-00679-7","DOI":"10.1007\/s10009-022-00679-7"},{"key":"15_CR17","doi-asserted-by":"publisher","unstructured":"Hubert, T., March\u00e9, C.: A case study of C source code verification: the Schorr-Waite algorithm. In: Third IEEE International Conference on Software Engineering and Formal Methods (SEFM 2005), 7-9 September 2005, Koblenz, Germany. pp. 190\u2013199 (2005). https:\/\/doi.org\/10.1109\/SEFM.2005.1","DOI":"10.1109\/SEFM.2005.1"},{"key":"15_CR18","doi-asserted-by":"publisher","unstructured":"Kassios, I.T.: The dynamic frames theory. Formal Aspects Comput. 23(3), 267\u2013288 (2011). https:\/\/doi.org\/10.1007\/s00165-010-0152-5","DOI":"10.1007\/s00165-010-0152-5"},{"key":"15_CR19","doi-asserted-by":"publisher","unstructured":"Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D.A., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: formal verification of an OS kernel. In: Proceedings of the 22nd ACM Symposium on Operating Systems Principles 2009, SOSP 2009, Big Sky, Montana, USA, October 11-14, 2009. pp. 207\u2013220 (2009). https:\/\/doi.org\/10.1145\/1629575.1629596","DOI":"10.1145\/1629575.1629596"},{"key":"15_CR20","doi-asserted-by":"publisher","unstructured":"Lammich, P.: Efficient verified implementation of introsort and pdqsort. In: Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part II. pp. 307\u2013323 (2020). https:\/\/doi.org\/10.1007\/978-3-030-51054-1_18","DOI":"10.1007\/978-3-030-51054-1_18"},{"key":"15_CR21","doi-asserted-by":"publisher","unstructured":"Lammich, P.: Refinement of parallel algorithms down to LLVM. In: 13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, Israel. pp. 24:1\u201324:18 (2022). https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2022.24","DOI":"10.4230\/LIPIcs.ITP.2022.24"},{"key":"15_CR22","unstructured":"Leavens, G.T., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D., M\u00fcller, P., Kiniry, J., Chalin, P., Zimmerman, D.M., et\u00a0al.: JML reference manual (2008)"},{"key":"15_CR23","doi-asserted-by":"publisher","unstructured":"Leinenbach, D., Santen, T.: Verifying the microsoft Hyper-V hypervisor with VCC. In: FM 2009: Formal Methods, Second World Congress, Eindhoven, The Netherlands, November 2-6, 2009. Proceedings. pp. 806\u2013809 (2009). https:\/\/doi.org\/10.1007\/978-3-642-05089-3_51","DOI":"10.1007\/978-3-642-05089-3_51"},{"key":"15_CR24","doi-asserted-by":"publisher","unstructured":"Leino, K.R.M.: Accessible software verification with Dafny. IEEE Softw. 34(6), 94\u201397 (2017). https:\/\/doi.org\/10.1109\/MS.2017.4121212","DOI":"10.1109\/MS.2017.4121212"},{"key":"15_CR25","unstructured":"Leino, K.R.M., Moskal, M.: Usable auto-active verification. Usable Verification Workshop, Redmond, WS (2010)"},{"key":"15_CR26","doi-asserted-by":"publisher","unstructured":"Mahboubi, A.: Proving formally the implementation of an efficient gcd algorithm for polynomials. In: Automated Reasoning, Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings. pp. 438\u2013452 (2006). https:\/\/doi.org\/10.1007\/11814771_37","DOI":"10.1007\/11814771_37"},{"key":"15_CR27","doi-asserted-by":"publisher","unstructured":"Medina-Bulo, I., Palomo-Lozano, F., Ruiz-Reina, J.: A verified common lisp implementation of Buchberger\u2019s algorithm in ACL2. J. Symb. Comput. 45(1), 96\u2013123 (2010). https:\/\/doi.org\/10.1016\/j.jsc.2009.07.002","DOI":"10.1016\/j.jsc.2009.07.002"},{"key":"15_CR28","doi-asserted-by":"publisher","unstructured":"Mehta, F., Nipkow, T.: Proving pointer programs in higher-order logic. In: Automated Deduction - CADE-19, 19th International Conference on Automated Deduction Miami Beach, FL, USA, July 28 - August 2, 2003, Proceedings. pp. 121\u2013135 (2003). https:\/\/doi.org\/10.1007\/978-3-540-45085-6_10","DOI":"10.1007\/978-3-540-45085-6_10"},{"key":"15_CR29","doi-asserted-by":"publisher","unstructured":"Meyer, B.: Applying \"design by contract\". Computer 25(10), 40\u201351 (1992). https:\/\/doi.org\/10.1109\/2.161279","DOI":"10.1109\/2.161279"},{"key":"15_CR30","doi-asserted-by":"publisher","unstructured":"Mohan, A., Leow, W.X., Hobor, A.: Functional correctness of C implementations of Dijkstra\u2019s, Kruskal\u2019s, and Prim\u2019s algorithms. In: Computer Aided Verification - 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part II. pp. 801\u2013826 (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_37","DOI":"10.1007\/978-3-030-81688-9_37"},{"key":"15_CR31","doi-asserted-by":"publisher","unstructured":"Mommen, N., Jacobs, B.: Verification of C++ programs with VeriFast. CoRR abs\/2212.13754 (2022). https:\/\/doi.org\/10.48550\/arXiv.2212.13754","DOI":"10.48550\/arXiv.2212.13754"},{"key":"15_CR32","doi-asserted-by":"publisher","unstructured":"Mostowski, W., Ulbrich, M.: Dynamic dispatch for method contracts through abstract predicates. LNCS Trans. Modul. Compos. 1, 238\u2013267 (2016). https:\/\/doi.org\/10.1007\/978-3-319-46969-0_7","DOI":"10.1007\/978-3-319-46969-0_7"},{"key":"15_CR33","doi-asserted-by":"publisher","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.S.: Z3: an efficient SMT solver. In: Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings. pp. 337\u2013340 (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"15_CR34","doi-asserted-by":"publisher","unstructured":"Safari, M., Huisman, M.: A generic approach to the verification of the permutation property of sequential and parallel swap-based sorting algorithms. In: Integrated Formal Methods - 16th International Conference, IFM 2020, Lugano, Switzerland, November 16-20, 2020, Proceedings. pp. 257\u2013275 (2020). https:\/\/doi.org\/10.1007\/978-3-030-63461-2_14","DOI":"10.1007\/978-3-030-63461-2_14"},{"key":"15_CR35","doi-asserted-by":"publisher","unstructured":"Tschannen, J., Furia, C.A., Nordio, M., Polikarpova, N.: Autoproof: Auto-active functional verification of object-oriented programs. In: Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings. pp. 566\u2013580 (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_53","DOI":"10.1007\/978-3-662-46681-0_53"},{"key":"15_CR36","doi-asserted-by":"publisher","unstructured":"Wassenberg, J., Blacher, M., Giesen, J., Sanders, P.: Vectorized and performance-portable quicksort. Softw. Pract. Exp. 52(12), 2684\u20132699 (2022). https:\/\/doi.org\/10.1002\/spe.3142","DOI":"10.1002\/spe.3142"},{"key":"15_CR37","doi-asserted-by":"publisher","unstructured":"Xu, F., Fu, M., Feng, X., Zhang, X., Zhang, H., Li, Z.: A practical verification framework for preemptive OS kernels. In: Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part II. pp. 59\u201379 (2016). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_4","DOI":"10.1007\/978-3-319-41540-6_4"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-57246-3_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,3]],"date-time":"2024-04-03T14:08:53Z","timestamp":1712153333000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-57246-3_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031572456","9783031572463"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-57246-3_15","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":"4 April 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","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":"6 April 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2024\/conferences\/tacas\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"159","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"53","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"16","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"33% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"10","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}