Abstract
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 language | English |
---|---|
Title of host publication | Programming Languages and Systems |
Subtitle of host publication | 30th 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 |
Editors | Nobuko Yoshida |
Place of Publication | Cham |
Publisher | Springer |
Pages | 292-319 |
Number of pages | 28 |
ISBN (Electronic) | 978-3-030-72019-3 |
ISBN (Print) | 978-3-030-72018-6 |
DOIs | |
Publication status | Published - 2021 |
Externally published | Yes |
Event | 30th European Symposium on Programming, ESOP 2021 - Online Conference, Luxembourg Duration: 27 Mar 2021 → 1 Apr 2021 Conference number: 30 |
Publication series
Name | Lecture Notes in Computer Science |
---|---|
Publisher | Springer |
Volume | 12648 |
ISSN (Print) | 0302-9743 |
ISSN (Electronic) | 1611-3349 |
Conference
Conference | 30th European Symposium on Programming, ESOP 2021 |
---|---|
Abbreviated title | ESOP 2021 |
Country/Territory | Luxembourg |
City | Online Conference |
Period | 27/03/21 → 1/04/21 |
Keywords
- Algorithm analysis
- Program verification
- Refinement