Where academic tradition
meets the exciting future

Compositional Specification and Analysis of Cost-Based Properties in Probabilistic Programs

Orieta Celiku, Annabelle McIver, Compositional Specification and Analysis of Cost-Based Properties in Probabilistic Programs. In: Ian J. Hayes Andrzej Tarlecki John Fitzgerald (Ed.), FM 2005: Formal Methods: International Symposium of Formal Methods Europe, Newcastle, UK, July 18-22, 2005. Proceedings, Lecture Notes in Computer Science 3582, 107–122, Springer-Verlag, 2005.

Abstract:

We introduce a formal framework for reasoning about performance-style
properties of probabilistic programs at the level of program code.
Drawing heavily on the refinement-style of program verification, our
approach promotes abstraction and proof re-use. The theory and proof
tools to facilitate the verification have been implemented in HOL.

BibTeX entry:

@INPROCEEDINGS{inpCeMc05a,
  title = {Compositional Specification and Analysis of Cost-Based Properties in Probabilistic Programs},
  booktitle = {FM 2005: Formal Methods: International Symposium of Formal Methods Europe, Newcastle, UK, July 18-22, 2005. Proceedings},
  author = {Celiku, Orieta and McIver, Annabelle},
  volume = {3582},
  series = {Lecture Notes in Computer Science},
  editor = {John Fitzgerald, Ian J. Hayes Andrzej Tarlecki},
  publisher = {Springer-Verlag},
  pages = {107–122},
  year = {2005},
}

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

Publication Forum rating of this publication: level 1

Edit publication