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. In: Proceedings of the 15th Nordic Workshop on Programming Theory , Ser. B, 2003.

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:

@INPROCEEDINGS{inpCeMc03a,
  title = {Cost-Based Analysis of Probabilistic Programs Mechanised in HOL},
  booktitle = {Proceedings of the 15th Nordic Workshop on Programming Theory },
  author = {Celiku, Orieta and McIver, Annabelle},
  number = {34},
  series = {Ser. B},
  year = {2003},
}

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

Edit publication