Remember Me
Or use your Academic/Social account:


Or use your Academic/Social account:


You have just completed your registration at OpenAire.

Before you can login to the site, you will need to activate your account. An e-mail will be sent to you with the proper instructions.


Please note that this site is currently undergoing Beta testing.
Any new content you create is not guaranteed to be present to the final version of the site upon release.

Thank you for your patience,
OpenAire Dev Team.

Close This Message


Verify Password:
Verify E-mail:
*All Fields Are Required.
Please Verify You Are Human:
fbtwitterlinkedinvimeoflicker grey 14rssslideshare1
Publisher: Springer Berlin / Heidelberg
Languages: English
Types: Other
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.
  • The results below are discovered through our pilot algorithms. Let us know how we are doing!

    • 1. S. Andova, H. Hermanns, and J.-P. Katoen. Discrete-time rewards model-checked. In FORMATS 2003, volume 2791 of LNCS, pages 88-104. Springer, 2004.
    • 2. R. Calinescu, C. Ghezzi, K. Johnson, M. Pezze, Y. Rafiq, and G. Tamburrelli. Formal verification with confidence intervals to establish quality of service properties of software systems. IEEE Transactions on Reliability, PP:1-16, August 2015.
    • 3. R. Calinescu, K. Johnson, and Y. Rafiq. Developing self-verifying service-based systems. In ASE'13, pages 734-737, 2013.
    • 4. R. Calinescu, Y. Rafiq, K. Johnson, and M. E. Bakir. Adaptive model learning for continual verification of non-functional properties. In ICPE'14, pages 87-98, 2014.
    • 5. C. Dehnert, S. Junges, N. Jansen, F. Corzilius, M. Volk, H. Bruintjes, J.-P. Katoen, and E. Abraham. PROPhESY: A PRObabilistic ParamEter SYnthesis Tool. In CAV'15, volume 9206 of LNCS, pages 214-231. Springer, 2015.
    • 6. E. M. Hahn, H. Hermanns, B. Wachter, and L. Zhang. PARAM: A model checker for parametric Markov models. In CAV'10, pages 660-664, 2010.
    • 7. H. Hansson and B. Jonsson. A logic for reasoning about time and reliability. Formal Aspects of Computing, 6(5):512-535, 1994.
    • 8. B. R. Haverkort, J.-P. Katoen, and K. G. Larsen. Quantitative verification in practice. In ISoLA'10, volume 6416 of LNCS, page 127. Springer, 2010.
    • 9. J.-P. Katoen, I. S. Zapreev, E. M. Hahn, H. Hermanns, and D. N. Jansen. The ins and outs of the probabilistic model checker MRMC. Performance Evaluation, 68(2):90-104, 2011.
    • 10. M. Kwiatkowska, G. Norman, and D. Parker. PRISM 4.0: Verification of probabilistic real-time systems. In CAV'11, volume 6806 of LNCS, pages 585-591, 2011.
    • 11. M. Z. Kwiatkowska. Quantitative verification: Models, techniques and tools. In ESEC-FSE'07, pages 449-458, 2007.
    • 12. K.-S. Kwong and B. Iglewicz. On singular multivariate normal distribution and its applications. Computational statistics & data analysis, 22(3):271-285, 1996.
    • 13. J. Lo¨fberg. Automatic robust convex programming. Optimization methods and software, 27(1):115-129, 2012.
    • 14. G. Norman and D. Parker. Quantitative verification: Formal guarantees for timeliness, reliability and performance. Technical report, London Mathematical Society and the Smith Institute for Industrial Mathematics and System Engineering, 2014.
    • 15. G. Su and D. Rosenblum. Asymptotic bounds for quantitative verification of perturbed probabilistic systems. In ICFEM'13, pages 297-312. Springer, 2013.
  • No related research data.
  • No similar publications.

Share - Bookmark

Cite this article