Proofs and refutations for probabilistic refinement

A. K. McIver; C. C. Morgan; C. Gonzalia

doi:10.1007/978-3-540-68237-0_9

Proofs and refutations for probabilistic refinement

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

School of Computing

Research output: Contribution to journal › Article › peer-review

5 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 language	English
Pages (from-to)	100-115
Number of pages	16
Journal	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	5014 LNCS
DOIs	https://doi.org/10.1007/978-3-540-68237-0_9
Publication status	Published - 2008

Access to Document

10.1007/978-3-540-68237-0_9

Cite this

@article{00dcae89abd245bc9eefc71f546c1b5f,

title = "Proofs and refutations for probabilistic refinement",

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.",

author = "McIver, {A. K.} and Morgan, {C. C.} and C. Gonzalia",

year = "2008",

doi = "10.1007/978-3-540-68237-0_9",

language = "English",

volume = "5014 LNCS",

pages = "100--115",

journal = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

issn = "0302-9743",

publisher = "Springer, Springer Nature",

}

TY - JOUR

T1 - Proofs and refutations for probabilistic refinement

AU - McIver, A. K.

AU - Morgan, C. C.

AU - Gonzalia, C.

PY - 2008

Y1 - 2008

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=47249092810&partnerID=8YFLogxK

U2 - 10.1007/978-3-540-68237-0_9

DO - 10.1007/978-3-540-68237-0_9

M3 - Article

AN - SCOPUS:47249092810

SN - 0302-9743

VL - 5014 LNCS

SP - 100

EP - 115

JO - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

JF - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

ER -

Proofs and refutations for probabilistic refinement

Abstract

Access to Document

Other files and links

Fingerprint

Cite this