Forskning ved Københavns Universitet - Københavns Universitet


A flow calculus of mwp-bounds for complexity analysis

Publikation: Bidrag til tidsskriftTidsskriftartikel

  • Neil Jones
  • Lars Kristiansen

We present a method for certifying that the values computed by an imperative program will be bounded by polynomials in the program's inputs. To this end, we introduce mwp-matrices and define a semantic relation ⊧ C : M, where C is a program and M is an mwp-matrix. It follows straightforwardly from our definitions that there exists M such that ⊧ C : M holds iff every value computed by C is bounded by a polynomial in the inputs. Furthermore, we provide a syntactical proof calculus and define the relation ⊢ C : M to hold iff there exists a derivation in the calculus where C : M is the bottom line. We prove that ⊢ C : M implies ⊧ C : M.

By means of exhaustive proof search, an algorithm can decide if there exists M such that the relation ⊢ C : M holds, and thus, our results yield a computational method.

TidsskriftACM Transactions on Computational Logic
Udgave nummer4
Antal sider41
StatusUdgivet - 2010

ID: 21430198