{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T10:14:55Z","timestamp":1742379295877},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662496732"},{"type":"electronic","value":"9783662496749"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-662-49674-9_32","type":"book-chapter","created":{"date-parts":[[2016,4,8]],"date-time":"2016-04-08T18:49:00Z","timestamp":1460141340000},"page":"540-546","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":17,"title":["FACT: A Probabilistic Model Checker for Formal Verification with Confidence Intervals"],"prefix":"10.1007","author":[{"given":"Radu","family":"Calinescu","sequence":"first","affiliation":[]},{"given":"Kenneth","family":"Johnson","sequence":"additional","affiliation":[]},{"given":"Colin","family":"Paterson","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,4,9]]},"reference":[{"key":"32_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/978-3-540-40903-8_8","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"S Andova","year":"2003","unstructured":"Andova, S., Hermanns, H., Katoen, J.-P.: Discrete-time rewards model-checked. FORMATS 2003. LNCS, vol. 2791, pp. 88\u2013104. Springer, Heidelberg (2003)"},{"issue":"99","key":"32_CR2","first-page":"1","volume":"PP","author":"R Calinescu","year":"2015","unstructured":"Calinescu, R., Ghezzi, C., Johnson, K., Pezze, M., Rafiq, Y., Tamburrelli, G.: Formal verification with confidence intervals to establish quality of service properties of software systems. IEEE Trans. Reliab. PP(99), 1\u201316 (2015)","journal-title":"IEEE Trans. Reliab."},{"key":"32_CR3","doi-asserted-by":"crossref","unstructured":"Calinescu, R., Johnson, K., Rafiq, Y.: Developing self-verifying service-based systems. In: ASE 2013, pp. 734\u2013737 (2013)","DOI":"10.1109\/ASE.2013.6693145"},{"key":"32_CR4","doi-asserted-by":"crossref","unstructured":"Calinescu, R., Rafiq, Y., Johnson, K., Bakir, M.E.: Adaptive model learning for continual verification of non-functional properties. In: ICPE 2014, pp. 87\u201398 (2014)","DOI":"10.1145\/2568088.2568094"},{"key":"32_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/978-3-319-21690-4_13","volume-title":"Computer Aided Verification","author":"C Dehnert","year":"2015","unstructured":"Dehnert, C., Junges, S., Jansen, N., Corzilius, F., Volk, M., Bruintjes, H., Katoen, J.-P., \u00c1brah\u00e1m, E.: PROPhESY: A PRObabilistic ParamEter SYnthesis Tool. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 214\u2013231. Springer, Heidelberg (2015)"},{"key":"32_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"660","DOI":"10.1007\/978-3-642-14295-6_56","volume-title":"Computer Aided Verification","author":"EM Hahn","year":"2010","unstructured":"Hahn, E.M., Hermanns, H., Wachter, B., Zhang, L.: PARAM: a model checker for parametric Markov models. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 660\u2013664. Springer, Heidelberg (2010)"},{"issue":"5","key":"32_CR7","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H Hansson","year":"1994","unstructured":"Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects Comput. 6(5), 512\u2013535 (1994)","journal-title":"Formal Aspects Comput."},{"key":"32_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/978-3-642-16561-0_17","volume-title":"Leveraging Applications of Formal Methods, Verification, and Validation","author":"BR Haverkort","year":"2010","unstructured":"Haverkort, B.R., Katoen, J.-P., Larsen, K.G.: Quantitative verification in practice. In: Margaria, T., Steffen, B. (eds.) ISoLA 2010, Part II. LNCS, vol. 6416, pp. 127\u2013127. Springer, Heidelberg (2010)"},{"issue":"2","key":"32_CR9","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1016\/j.peva.2010.04.001","volume":"68","author":"J-P Katoen","year":"2011","unstructured":"Katoen, J.-P., Zapreev, I.S., Hahn, E.M., Hermanns, H., Jansen, D.N.: The ins and outs of the probabilistic model checker MRMC. Perform. Eval. 68(2), 90\u2013104 (2011)","journal-title":"Perform. Eval."},{"key":"32_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585\u2013591. Springer, Heidelberg (2011)"},{"key":"32_CR11","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M.Z.: Quantitative verification: models, techniques and tools. In: ESEC-FSE 2007, pp. 449\u2013458 (2007)","DOI":"10.1145\/1287624.1287688"},{"issue":"3","key":"32_CR12","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1016\/0167-9473(95)00050-X","volume":"22","author":"K-S Kwong","year":"1996","unstructured":"Kwong, K.-S., Iglewicz, B.: On singular multivariate normal distribution and its applications. Comput. Stat. Data Anal. 22(3), 271\u2013285 (1996)","journal-title":"Comput. Stat. Data Anal."},{"issue":"1","key":"32_CR13","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1080\/10556788.2010.517532","volume":"27","author":"J L\u00f6fberg","year":"2012","unstructured":"L\u00f6fberg, J.: Automatic robust convex programming. Optim. Methods Softw. 27(1), 115\u2013129 (2012)","journal-title":"Optim. Methods Softw."},{"key":"32_CR14","unstructured":"Norman, G., Parker, D.: 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)"},{"key":"32_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/978-3-642-41202-8_20","volume-title":"Formal Methods and Software Engineering","author":"G Su","year":"2013","unstructured":"Su, G., Rosenblum, D.S.: Asymptotic bounds for quantitative verification of perturbed probabilistic systems. In: Groves, L., Sun, J. (eds.) ICFEM 2013. LNCS, vol. 8144, pp. 297\u2013312. Springer, Heidelberg (2013)"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-49674-9_32","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,3,24]],"date-time":"2020-03-24T01:15:21Z","timestamp":1585012521000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-49674-9_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783662496732","9783662496749"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-49674-9_32","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"9 April 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}