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

Orieta Celiku^*, Annabelle McIver

^*Corresponding author for this work

School of Computing

Research output: Contribution to journal › Article › peer-review

14 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 language	English
Pages (from-to)	107-122
Number of pages	16
Journal	Lecture Notes in Computer Science
Volume	3582
Publication status	Published - 2005

Cite this

@article{c4c199918655440bbeeca3bb1a4000fa,

title = "Compositional specification and analysis of cost-based properties in probabilistic programs",

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.",

author = "Orieta Celiku and Annabelle McIver",

year = "2005",

language = "English",

volume = "3582",

pages = "107--122",

journal = "Lecture Notes in Computer Science",

issn = "0302-9743",

publisher = "Springer, Springer Nature",

}

TY - JOUR

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

AU - Celiku, Orieta

AU - McIver, Annabelle

PY - 2005

Y1 - 2005

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=26444519171&partnerID=8YFLogxK

M3 - Article

AN - SCOPUS:26444519171

SN - 0302-9743

VL - 3582

SP - 107

EP - 122

JO - Lecture Notes in Computer Science

JF - Lecture Notes in Computer Science

ER -

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

Abstract

Other files and links

Fingerprint

Cite this