Proofs and refutations for probabilistic refinement
- 14:00 12th June 2008 ( week 8, Trinity Term 2008 )Room 051, Oxford University Computing Laboratory
We consider the issue of ﬁnding and presenting counterexamples to a claim "this spec is implemented by that imp", that is spec ⊑ imp (reﬁnement), in the context of probabilistic systems: using a geometric interpretation of the probabilistic/demonic semantic domain we are able to encode both reﬁnement success and reﬁnement failure as linear satisfaction problems, which can then be analysed automatically by an SMT solver. This allows the automatic discovery of certiﬁcates for counterexamples in independently and eﬃciently checkable form. In many cases the counterexamples can subsequently be converted into "source level" hints for the veriﬁer. These techniques have been used to establish key results for testing semantics in probabilistic concurrency.
 Proofs and refutations for probabilistic refinement, McIver, Morgan and Gonzalia, Proceedings of Formal Methods 2008
 Scalar outcomes suffice for finitary probabilistic testing, Deng, van Glabeek, Morgan and Zhang, Proceedings of ESOP 2007.