%A Emre Yilmaz
%A Thai Son Hoang
%T Development of Rabin's Choice Coordination Algorithm in Event-B
%X The paper reports our investigation on tool support for the integration of qualitative probabilistic reasoning into Event-B.  In the process, we formalise a non-trivial algorithm, namely Rabin's choice coordination.  Our correctness reasoning is a combination of termination proofs in terms of probabilistic convergence and standard invariant techniques.  Moreover, we describe how qualitative probabilistic reasoning can be maintained during refinement.
%C Dusseldorf, Germany
%I University of D?sseldorf
%L deploy258

<script src='//archive-bar.soton.ac.uk/archive-bar.js'></script>