For a Few Dollars More: Verified Fine-Grained Algorithm Analysis Down to LLVM

Maximilian P.L. Haslbeck*, Peter Lammich

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

6 Citations (Scopus)
32 Downloads (Pure)


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 resource currencies 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 O(nlog n) 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.

Original languageEnglish
Title of host publicationProgramming Languages and Systems
Subtitle of host publication30th European Symposium on Programming, ESOP 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 – April 1, 2021, Proceedings
EditorsNobuko Yoshida
Place of PublicationCham
Number of pages28
ISBN (Electronic)978-3-030-72019-3
ISBN (Print)978-3-030-72018-6
Publication statusPublished - 2021
Externally publishedYes
Event30th European Symposium on Programming, ESOP 2021 - Online Conference, Luxembourg
Duration: 27 Mar 20211 Apr 2021
Conference number: 30

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference30th European Symposium on Programming, ESOP 2021
Abbreviated titleESOP 2021
CityOnline Conference


  • Algorithm analysis
  • Program verification
  • Refinement


Dive into the research topics of 'For a Few Dollars More: Verified Fine-Grained Algorithm Analysis Down to LLVM'. Together they form a unique fingerprint.

Cite this