Proofs and refutations for probabilistic refinement

A. K. McIver, C. C. Morgan, C. Gonzalia

Research output: Contribution to journalArticle

4 Citations (Scopus)

Abstract

We consider the issue of finding and presenting counterexamples to a claim "this spec is implemented by that imp", that is (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. 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.

Original languageEnglish
Pages (from-to)100-115
Number of pages16
JournalLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume5014 LNCS
DOIs
Publication statusPublished - 2008

Fingerprint Dive into the research topics of 'Proofs and refutations for probabilistic refinement'. Together they form a unique fingerprint.

  • Cite this