Where academic tradition
meets the exciting future

Cost-Based Analysis of Probabilistic Programs Mechanised in HOL

Orieta Celiku, Annabelle McIver, Cost-Based Analysis of Probabilistic Programs Mechanised in HOL. Nordic Journal of Computing 11(2), 102–128, 2004.

Abstract:

We provide a HOL formalisation for analysing expected time bounds for
probabilistic programs. Our formalisation is based on the quantitative
program logic of Morgan et al. and McIver's extension of it to include
performance-style operators. In addition we provide some novel results
based on probabilistic data refinement which we use to improve the
utility of the basic method.

BibTeX entry:

@ARTICLE{jCeMc04a,
  title = {Cost-Based Analysis of Probabilistic Programs Mechanised in HOL},
  author = {Celiku, Orieta and McIver, Annabelle},
  journal = {Nordic Journal of Computing},
  volume = {11},
  number = {2},
  pages = {102–128},
  year = {2004},
}

Belongs to TUCS Research Unit(s): Learning and Reasoning Lab

Publication Forum rating of this publication: level 1

Edit publication