Correctness by construction for probabilistic programs

Annabelle McIver*, Carroll Morgan

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference proceeding contribution

1 Citation (Scopus)

Abstract

The “correct by construction” paradigm is an important component of modern Formal Methods, and here we use the probabilistic Guarded-Command Language pGCL to illustrate its application to probabilistic programming. 

pGCL extends Dijkstra’s guarded-command language GCL with probabilistic choice, and is equipped with a correctness-preserving refinement relation (⊆) that enables compact, abstract specifications of probabilistic properties to be transformed gradually to concrete, executable code by applying mathematical insights in a systematic and layered way. 

Characteristically for correctness by construction, as far as possible the reasoning in each refinement-step layer does not depend on earlier layers, and does not affect later ones. 

We demonstrate the technique by deriving a fair-coin implementation of any given discrete probability distribution. In the special case of simulating a fair die, our correct-by-construction algorithm turns out to be “within spitting distance” of Knuth and Yao’s optimal solution.

Original languageEnglish
Title of host publicationLeveraging Applications of Formal Methods, Verification and Validation
Subtitle of host publicationVerification Principles - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Proceedings
EditorsTiziana Margaria, Bernhard Steffen
Place of PublicationCham, Switzerland
PublisherSpringer, Springer Nature
Pages216-239
Number of pages24
ISBN (Electronic)9783030613624
ISBN (Print)9783030613617
DOIs
Publication statusPublished - 2020
Event9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2020 - Rhodes, Greece
Duration: 20 Oct 202030 Oct 2020

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume12476 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2020
CountryGreece
CityRhodes
Period20/10/2030/10/20

Fingerprint Dive into the research topics of 'Correctness by construction for probabilistic programs'. Together they form a unique fingerprint.

Cite this