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.
|Number of pages||16|
|Journal||Lecture Notes in Computer Science|
|Publication status||Published - 2005|