We use cookies to ensure that we give you the best experience on our website Learn more

Home

Saved research

Submission

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

Submitted

8 Views
0 Downloads
0 Saves

Presentation

thumbnail

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(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.

Datasets

No datasets are available for this submission.

Morressier

Company

Legal

Follow us

© Copyright 2021 Morressier GmbH. All rights reserved.

Morressier

© Copyright 2021 Morressier GmbH.
All rights reserved.