{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T16:17:29Z","timestamp":1743092249576,"version":"3.40.3"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030720186"},{"type":"electronic","value":"9783030720193"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,3,23]],"date-time":"2021-03-23T00:00:00Z","timestamp":1616457600000},"content-version":"vor","delay-in-days":81,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We present a framework to verify both, functional correctness and worst-case complexity of practically efficient algorithms. We implemented a stepwise refinement approach, using the novel concept of <jats:italic>resource currencies<\/jats:italic> to naturally structure the resource analysis along the refinement chain, and allow a fine-grained analysis of operation counts. Our framework targets the LLVM intermediate representation. We extend its semantics from earlier work with a cost model. As case study, we verify the correctness and <jats:inline-formula><jats:alternatives><jats:tex-math>$$O(n\\log n)$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mi>O<\/mml:mi>\n                    <mml:mo>(<\/mml:mo>\n                    <mml:mi>n<\/mml:mi>\n                    <mml:mo>log<\/mml:mo>\n                    <mml:mi>n<\/mml:mi>\n                    <mml:mo>)<\/mml:mo>\n                  <\/mml:mrow>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula> worst-case complexity of an implementation of the introsort algorithm, whose performance is on par with the state-of-the-art implementation found in the GNU C++ Library.<\/jats:p>","DOI":"10.1007\/978-3-030-72019-3_11","type":"book-chapter","created":{"date-parts":[[2021,3,22]],"date-time":"2021-03-22T14:03:10Z","timestamp":1616421790000},"page":"292-319","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["For a Few Dollars More"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4306-869X","authenticated-orcid":false,"given":"Maximilian P. L.","family":"Haslbeck","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3576-0504","authenticated-orcid":false,"given":"Peter","family":"Lammich","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,3,23]]},"reference":[{"key":"11_CR1","doi-asserted-by":"publisher","unstructured":"Atkey, R.: Amortised resource analysis with separation logic. In: Gordon, A.D. (ed.) European Symposium on Programming, ESOP 2010. Lecture Notes in Computer Science, vol.\u00a06012, pp. 85\u2013103. Springer (2010). https:\/\/doi.org\/10.1007\/978-3-642-11957-6_6, https:\/\/doi.org\/10.1007\/978-3-642-11957-6_6","DOI":"10.1007\/978-3-642-11957-6_6"},{"key":"11_CR2","doi-asserted-by":"publisher","unstructured":"Blazy, S., Leroy, X.: Mechanized semantics for the Clight subset of the C language. J. Autom. Reason. 43(3), 263\u2013288 (2009). https:\/\/doi.org\/10.1007\/s10817-009-9148-3, https:\/\/doi.org\/10.1007\/s10817-009-9148-3","DOI":"10.1007\/s10817-009-9148-3"},{"key":"11_CR3","doi-asserted-by":"publisher","unstructured":"Calcagno, C., O\u2019Hearn, P.W., Yang, H.: Local action and abstract separation logic. In: Symposium on Logic in Computer Science (LICS 2007). pp. 366\u2013378. IEEE Computer Society (2007). https:\/\/doi.org\/10.1109\/LICS.2007.30, https:\/\/doi.org\/10.1109\/LICS.2007.30","DOI":"10.1109\/LICS.2007.30"},{"key":"11_CR4","doi-asserted-by":"publisher","unstructured":"Carbonneaux, Q., Hoffmann, J., Ramananandro, T., Shao, Z.: End-to-end verification of stack-space bounds for C programs. In: O\u2019Boyle, M.F.P., Pingali, K. (eds.) ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI \u201914, Edinburgh, United Kingdom - June 09 - 11, 2014. pp. 270\u2013281. ACM (2014). https:\/\/doi.org\/10.1145\/2594291.2594301, https:\/\/doi.org\/10.1145\/2594291.2594301","DOI":"10.1145\/2594291.2594301"},{"key":"11_CR5","doi-asserted-by":"publisher","unstructured":"Chargu\u00e9raud, A.: Separation logic for sequential programs (functional pearl). Proc. ACM Program. Lang. 4(ICFP), 116:1\u2013116:34 (2020). https:\/\/doi.org\/10.1145\/3408998, https:\/\/doi.org\/10.1145\/3408998","DOI":"10.1145\/3408998"},{"key":"11_CR6","doi-asserted-by":"publisher","unstructured":"Chargu\u00e9raud, A., Pottier, F.: Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits. J. Autom. Reason. 62(3), 331\u2013365 (2019). https:\/\/doi.org\/10.1007\/s10817-017-9431-7, https:\/\/doi.org\/10.1007\/s10817-017-9431-7","DOI":"10.1007\/s10817-017-9431-7"},{"key":"11_CR7","unstructured":"cppreference: C++ standard library specification of sort. https:\/\/en.cppreference.com\/w\/cpp\/algorithm\/sort, accessed: 2020-10-12"},{"key":"11_CR8","unstructured":"The GNU C++ library, https:\/\/gcc.gnu.org\/onlinedocs\/libstdc++\/, version 7.4.0"},{"key":"11_CR9","doi-asserted-by":"publisher","unstructured":"Gu\u00e9neau, A., Chargu\u00e9raud, A., Pottier, F.: A fistful of dollars: Formalizing asymptotic complexity claims via deductive program verification. In: Ahmed, A. (ed.) Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018. Lecture Notes in Computer Science, vol. 10801, pp. 533\u2013560. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-89884-1_19, https:\/\/doi.org\/10.1007\/978-3-319-89884-1_19","DOI":"10.1007\/978-3-319-89884-1_19"},{"key":"11_CR10","doi-asserted-by":"publisher","unstructured":"Gu\u00e9neau, A., Jourdan, J., Chargu\u00e9raud, A., Pottier, F.: Formal proof and analysis of an incremental cycle detection algorithm. In: Harrison, J., O\u2019Leary, J., Tolmach, A. (eds.) 10th International Conference on Interactive Theorem Proving, ITP 2019. LIPIcs, vol.\u00a0141, pp. 18:1\u201318:20. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2019). https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2019.18, https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2019.18","DOI":"10.4230\/LIPIcs.ITP.2019.18"},{"key":"11_CR11","doi-asserted-by":"publisher","unstructured":"Haslbeck, M.P.L., Lammich, P.: Refinement with time - refining the run-time of algorithms in Isabelle\/HOL. In: Harrison, J., O\u2019Leary, J., Tolmach, A. (eds.) 10th International Conference on Interactive Theorem Proving, ITP 2019. LIPIcs, vol.\u00a0141, pp. 20:1\u201320:18. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2019). https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2019.20, https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2019.20","DOI":"10.4230\/LIPIcs.ITP.2019.20"},{"key":"11_CR12","doi-asserted-by":"publisher","unstructured":"Hoare, C.A.R.: Algorithm 64: Quicksort. Commun. ACM 4(7), 321\u2013 (Jul 1961). https:\/\/doi.org\/10.1145\/366622.366644, https:\/\/doi.org\/10.1145\/366622.366644","DOI":"10.1145\/366622.366644"},{"key":"11_CR13","doi-asserted-by":"publisher","unstructured":"Krauss, A.: Recursive definitions of monadic functions. In: Bove, A., Komendantskaya, E., Niqui, M. (eds.) Proceedings Workshop on Partiality and Recursion in Interactive Theorem Provers, PAR 2010, Edinburgh, UK, 15th July 2010. EPTCS, vol.\u00a043, pp. 1\u201313 (2010). https:\/\/doi.org\/10.4204\/EPTCS.43.1, https:\/\/doi.org\/10.4204\/EPTCS.43.1","DOI":"10.4204\/EPTCS.43.1"},{"key":"11_CR14","doi-asserted-by":"publisher","unstructured":"Lammich, P.: Refinement to Imperative\/HOL. In: Urban, C., Zhang, X. (eds.) Interactive Theorem Proving - 6th International Conference, ITP 2015. Lecture Notes in Computer Science, vol.\u00a09236, pp. 253\u2013269. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-22102-1_17, https:\/\/doi.org\/10.1007\/978-3-319-22102-1_17","DOI":"10.1007\/978-3-319-22102-1_17"},{"key":"11_CR15","doi-asserted-by":"publisher","unstructured":"Lammich, P.: Generating verified LLVM from Isabelle\/HOL. In: Harrison, J., O\u2019Leary, J., Tolmach, A. (eds.) 10th International Conference on Interactive Theorem Proving, ITP 2019. LIPIcs, vol.\u00a0141, pp. 22:1\u201322:19. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2019). https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2019.22, https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2019.22","DOI":"10.4230\/LIPIcs.ITP.2019.22"},{"key":"11_CR16","doi-asserted-by":"publisher","unstructured":"Lammich, P.: Refinement to Imperative HOL. J. Autom. Reason. 62(4), 481\u2013503 (2019). https:\/\/doi.org\/10.1007\/s10817-017-9437-1, https:\/\/doi.org\/10.1007\/s10817-017-9437-1","DOI":"10.1007\/s10817-017-9437-1"},{"key":"11_CR17","doi-asserted-by":"publisher","unstructured":"Lammich, P.: Efficient verified implementation of introsort and pdqsort. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) IJCAR 2020. Lecture Notes in Computer Science, vol. 12167, pp. 307\u2013323. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-51054-1_18, https:\/\/doi.org\/10.1007\/978-3-030-51054-1_18","DOI":"10.1007\/978-3-030-51054-1_18"},{"key":"11_CR18","unstructured":"Lammich, P., Meis, R.: A Separation Logic Framework for Imperative HOL. Archive of Formal Proofs (Nov 2012), http:\/\/isa-afp.org\/entries\/Separation_Logic_Imperative_HOL.html, Formal proof development"},{"key":"11_CR19","doi-asserted-by":"publisher","unstructured":"Lammich, P., Tuerk, T.: Applying data refinement for monadic programs to Hopcroft\u2019s algorithm. In: Beringer, L., Felty, A.P. (eds.) Interactive Theorem Proving - Third International Conference, ITP 2012. Lecture Notesin Computer Science, vol.\u00a07406, pp. 166\u2013182. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-32347-8_12, https:\/\/doi.org\/10.1007\/978-3-642-32347-8_12","DOI":"10.1007\/978-3-642-32347-8_12"},{"key":"11_CR20","unstructured":"\u201dlibc++\u201d c++ standard library, https:\/\/libcxx.llvm.org\/"},{"key":"11_CR21","doi-asserted-by":"publisher","unstructured":"M\u00e9vel, G., Jourdan, J., Pottier, F.: Time credits and time receipts in Iris. In: Caires, L. (ed.) Programming Languages and Systems - 28th European Symposium on Programming, ESOP 2019. Lecture Notes in Computer Science, vol. 11423, pp. 3\u201329. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-17184-1_1, https:\/\/doi.org\/10.1007\/978-3-030-17184-1_1","DOI":"10.1007\/978-3-030-17184-1_1"},{"key":"11_CR22","doi-asserted-by":"crossref","unstructured":"Musser, D.R.: Introspective sorting and selection algorithms. Softw. Pract. Exp. 27(8), 983\u2013993 (1997)","DOI":"10.1002\/(SICI)1097-024X(199708)27:8<983::AID-SPE117>3.0.CO;2-#"},{"key":"11_CR23","doi-asserted-by":"publisher","unstructured":"Nipkow, T., Eberl, M., Haslbeck, M.P.L.: Verified textbook algorithms - A biased survey. In: Hung, D.V., Sokolsky, O. (eds.) Automated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020. Lecture Notes in Computer Science, vol. 12302, pp. 25\u201353. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-59152-6_2, https:\/\/doi.org\/10.1007\/978-3-030-59152-6_2","DOI":"10.1007\/978-3-030-59152-6_2"},{"key":"11_CR24","doi-asserted-by":"publisher","unstructured":"Wadler, P.: Comprehending monads. In: Proceedings of the 1990 ACM Conference on LISP and Functional Programming. p. 6178. LFP \u201990, Association for Computing Machinery, New York, NY, USA (1990). https:\/\/doi.org\/10.1145\/91556.91592, https:\/\/doi.org\/10.1145\/91556.91592","DOI":"10.1145\/91556.91592"},{"key":"11_CR25","doi-asserted-by":"publisher","unstructured":"Wang, P., Wang, D., Chlipala, A.: TiML: a functional language for practical complexity analysis with invariants. Proc. ACM Program. Lang. 1(OOPSLA), 79:1\u201379:26 (2017). https:\/\/doi.org\/10.1145\/3133903, https:\/\/doi.org\/10.1145\/3133903","DOI":"10.1145\/3133903"},{"key":"11_CR26","doi-asserted-by":"publisher","unstructured":"Zhan, B., Haslbeck, M.P.L.: Verifying asymptotic time complexity of imperative programs in Isabelle. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) Automated Reasoning - 9th International Joint Conference, IJCAR 2018. Lecture Notes in Computer Science, vol. 10900, pp. 532\u2013548. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-94205-6_35, https:\/\/doi.org\/10.1007\/978-3-319-94205-6_35","DOI":"10.1007\/978-3-319-94205-6_35"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-72019-3_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,25]],"date-time":"2021-10-25T03:07:10Z","timestamp":1635131230000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-72019-3_11"}},"subtitle":["Verified Fine-Grained Algorithm Analysis Down to LLVM"],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030720186","9783030720193"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-72019-3_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"23 March 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ESOP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Programming","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":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 March 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 April 2021","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":"esop2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2021\/esop","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-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":"79","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":"24","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":"0","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":"30% - 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-5","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)"}},{"value":"The conference took place virtually due to the COVID-19 pandemic","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}