Skip to main content

Proofs and refutations for probabilistic refinement

Annabelle McIver ( Macquarie University, Australia )

We consider the issue of finding and presenting counterexamples to a claim "this spec is implemented by that imp", that is spec ⊑ imp (refinement), in the context of probabilistic systems: using a geometric interpretation of the probabilistic/demonic semantic domain we are able to encode both refinement success and refinement failure as linear satisfaction problems, which can then be analysed automatically by an SMT solver[1]. This allows the automatic discovery of certificates for counterexamples in independently and efficiently checkable form. In many cases the counterexamples can subsequently be converted into "source level" hints for the verifier. These techniques have been used to establish key results for testing semantics in probabilistic concurrency[2].

[1] Proofs and refutations for probabilistic refinement, McIver, Morgan and Gonzalia, Proceedings of Formal Methods 2008

[2] Scalar outcomes suffice for finitary probabilistic testing, Deng, van Glabeek, Morgan and Zhang, Proceedings of ESOP 2007.

Share this: