Compositional specification and analysis of cost-based properties in probabilistic programs

Orieta Celiku*, Annabelle McIver

*Corresponding author for this work

Research output: Contribution to journalArticle

4 Citations (Scopus)

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.

Original languageEnglish
Pages (from-to)107-122
Number of pages16
JournalLecture Notes in Computer Science
Volume3582
Publication statusPublished - 2005

Fingerprint Dive into the research topics of 'Compositional specification and analysis of cost-based properties in probabilistic programs'. Together they form a unique fingerprint.

  • Cite this