For a Few Dollars More: Verified Fine-Grained Algorithm Analysis Down to LLVM
| Autor: | Maximilian P. L. Haslbeck, Peter Lammich |
|---|---|
| Přispěvatelé: | Formal Methods and Tools |
| Jazyk: | angličtina |
| Rok vydání: | 2022 |
| Předmět: |
Structure (mathematical logic)
Theoretical computer science Correctness Computer science Semantics (computer science) Resource analysis Introsort 020207 software engineering 02 engineering and technology Binary logarithm Resource (project management) Chain (algebraic topology) 020204 information systems 2023 OA procedure 0202 electrical engineering electronic engineering information engineering Software |
| Zdroj: | ACM Transactions on Programming Languages and Systems (TOPLAS), 44(3), 14:1-14:36. Association for Computing Machinery (ACM) Programming Languages and Systems ISBN: 9783030720186 ESOP |
| ISSN: | 0164-0925 |
| Popis: | 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(n\log n)$$ O ( n log 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|