Journal article icon

Journal article

On automated verification of probabilistic programs

Abstract:

We introduce a simple procedural probabilistic programming language which is suitable for coding a wide variety of randomised algorithms and protocols. This language is interpreted over finite datatypes and has a decidable equivalence problem. We have implemented an automated equivalence checker, which we call apex, for this language, based on game semantics. We illustrate our approach with three non-trivial case studies: (i) Herman's self-stabilisation algorithm; (ii) an analysis of the aver...

Expand abstract

Actions


Access Document


Authors


Murawski, AS More by this author
Ouaknine, J More by this author
More by this author
Institution:
University of Oxford
Department:
Oxford, MPLS, Computer Science
Journal:
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume:
4963 LNCS
Pages:
173-187
Publication date:
2008
DOI:
EISSN:
1611-3349
ISSN:
0302-9743
URN:
uuid:40ce31bb-86f4-4802-a2f0-0344bf0476b9
Source identifiers:
291604
Local pid:
pubs:291604
Language:
English

Terms of use


Metrics



If you are the owner of this record, you can report an update to it here: Report update to this record

TO TOP