Selected article for: "art state and case study"

Author: Haslbeck, Maximilian P. L.; Lammich, Peter
Title: For a Few Dollars More: Verified Fine-Grained Algorithm Analysis Down to LLVM
  • Cord-id: t3l7zb51
  • Document date: 2021_3_23
  • ID: t3l7zb51
    Snippet: 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 cor
    Document: 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 [Formula: see text] 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.

    Search related documents:
    Co phrase search for related documents
    • Try single phrases listed below for: 1