Isabelle logo

Manuel Eberl

Chair for Logic and Verification

Prov­ing Di­vide and Con­quer Com­plex­it­ies in Isa­belle/­HOL

by Manuel Eberl

In: J. Autom. Reasoning (2016)

DOI:

10.1007/s10817-016-9378-0

Abstract:

The Akra–Bazzi method, a generalisation of the well-known Master Theorem, is a useful tool for analysing the complexity of Divide & Conquer algorithms. This work describes a formalisation of the Akra–Bazzi method (as generalised by Leighton) in the interactive theorem prover Isabelle/HOL and the derivation of a generalised version of the Master Theorem from it. We also provide some automated proof methods that facilitate the application of this Master Theorem and allow mostly automatic verification of Θ-bounds for Divide & Conquer recurrences.

To our knowledge, this is the first formalisation of theorems for the analysis of such recurrences.

Download preprint PDF (306 KiB)

BibTeX:

@Article{eberl17jar,
  author = "Manuel Eberl",
  title = "Proving Divide and Conquer Complexities in {I}sabelle/{HOL}",
  journal = "J. Autom. Reasoning",
  year = "2017",
  month = "Apr",
  day = "01",
  volume = "58",
  number = "4",
  pages = "483--508",
  doi = "10.1007/s10817-016-9378-0",
  issn = "1573-0670"
}

Download BibTeX (320 Bytes)

(The final publication is available at link.springer.com)