Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

**FACT : A Probabilistic Model Checker for Formal Verification with Confidence Intervals.** / Calinescu, Radu Constantin; Johnson, Kenneth Harold Anthony; Paterson, Colin Alexander.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Calinescu, RC, Johnson, KHA & Paterson, CA 2016, FACT: A Probabilistic Model Checker for Formal Verification with Confidence Intervals. in *Tools and Algorithms for the Construction and Analysis of Systems: 22nd International Conference, TACAS 2016.* Lecture Notes in Computer Science (LNCS), vol. 9636, Springer Berlin / Heidelberg, pp. 540-546.

Calinescu, R. C., Johnson, K. H. A., & Paterson, C. A. (2016). FACT: A Probabilistic Model Checker for Formal Verification with Confidence Intervals. In *Tools and Algorithms for the Construction and Analysis of Systems: 22nd International Conference, TACAS 2016 *(pp. 540-546). (Lecture Notes in Computer Science (LNCS); Vol. 9636). Springer Berlin / Heidelberg.

Calinescu RC, Johnson KHA, Paterson CA. FACT: A Probabilistic Model Checker for Formal Verification with Confidence Intervals. In Tools and Algorithms for the Construction and Analysis of Systems: 22nd International Conference, TACAS 2016. Springer Berlin / Heidelberg. 2016. p. 540-546. (Lecture Notes in Computer Science (LNCS)).

@inproceedings{457c371e1a05428cb11410b4ea0fef38,

title = "FACT: A Probabilistic Model Checker for Formal Verification with Confidence Intervals",

abstract = "We introduce FACT, a probabilistic model checker that computes confidence intervals for the evaluated properties of Markov chains with unknown transition probabilities when observations of these transitions are available. FACT is unaffected by the unquantified estimation errors generated by the use of point probability estimates, a common practice that limits the applicability of quantitative verification. As such, FACT can prevent invalid decisions in the construction and analysis of systems, and extends the applicability of quantitative verification to domains in which unknown estimation errors are unacceptable.",

author = "Calinescu, {Radu Constantin} and Johnson, {Kenneth Harold Anthony} and Paterson, {Colin Alexander}",

note = "{\textcopyright} Springer-Verlag Berlin Heidelberg, 2016. This is an author-produced version of the published paper. Uploaded in accordance with the publisher{\textquoteright}s self-archiving policy. Further copying may not be permitted; contact the publisher for details",

year = "2016",

language = "English",

isbn = "9783662496749",

series = "Lecture Notes in Computer Science (LNCS)",

publisher = "Springer Berlin / Heidelberg",

pages = "540--546",

booktitle = "Tools and Algorithms for the Construction and Analysis of Systems: 22nd International Conference, TACAS 2016",

}

TY - GEN

T1 - FACT

T2 - A Probabilistic Model Checker for Formal Verification with Confidence Intervals

AU - Calinescu, Radu Constantin

AU - Johnson, Kenneth Harold Anthony

AU - Paterson, Colin Alexander

N1 - © Springer-Verlag Berlin Heidelberg, 2016. This is an author-produced version of the published paper. Uploaded in accordance with the publisher’s self-archiving policy. Further copying may not be permitted; contact the publisher for details

PY - 2016

Y1 - 2016

N2 - We introduce FACT, a probabilistic model checker that computes confidence intervals for the evaluated properties of Markov chains with unknown transition probabilities when observations of these transitions are available. FACT is unaffected by the unquantified estimation errors generated by the use of point probability estimates, a common practice that limits the applicability of quantitative verification. As such, FACT can prevent invalid decisions in the construction and analysis of systems, and extends the applicability of quantitative verification to domains in which unknown estimation errors are unacceptable.

AB - We introduce FACT, a probabilistic model checker that computes confidence intervals for the evaluated properties of Markov chains with unknown transition probabilities when observations of these transitions are available. FACT is unaffected by the unquantified estimation errors generated by the use of point probability estimates, a common practice that limits the applicability of quantitative verification. As such, FACT can prevent invalid decisions in the construction and analysis of systems, and extends the applicability of quantitative verification to domains in which unknown estimation errors are unacceptable.

UR - http://link.springer.com/chapter/10.1007%2F978-3-662-49674-9_32

M3 - Conference contribution

SN - 9783662496749

T3 - Lecture Notes in Computer Science (LNCS)

SP - 540

EP - 546

BT - Tools and Algorithms for the Construction and Analysis of Systems: 22nd International Conference, TACAS 2016

PB - Springer Berlin / Heidelberg

ER -