By the same authors

FACT: A Probabilistic Model Checker for Formal Verification with Confidence Intervals

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Full text download(s)



Publication details

Title of host publicationTools and Algorithms for the Construction and Analysis of Systems: 22nd International Conference, TACAS 2016
DatePublished - 2016
Number of pages7
PublisherSpringer Berlin / Heidelberg
Original languageEnglish
ISBN (Print)9783662496749

Publication series

NameLecture Notes in Computer Science (LNCS)
PublisherSpringer, Berlin, Heidelberg


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.

Bibliographical note

© 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

Discover related content

Find related publications, people, projects, datasets and more using interactive charts.

View graph of relations