{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:48:13Z","timestamp":1725490093156},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540745907"},{"type":"electronic","value":"9783540745914"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-74591-4_10","type":"book-chapter","created":{"date-parts":[[2007,8,22]],"date-time":"2007-08-22T14:49:52Z","timestamp":1187794192000},"page":"119-134","source":"Crossref","is-referenced-by-count":6,"title":["Verification of Expectation Properties for Discrete Random Variables in HOL"],"prefix":"10.1007","author":[{"given":"Osman","family":"Hasan","sequence":"first","affiliation":[]},{"given":"Sofi\u00e8ne","family":"Tahar","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"4","key":"10_CR1","doi-asserted-by":"publisher","first-page":"524","DOI":"10.1109\/TSE.2003.1205180","volume":"29","author":"C. Baier","year":"2003","unstructured":"Baier, C., Haverkort, B., Hermanns, H., Katoen, J.P.: Model Checking Algorithms for Continuous time Markov Chains. IEEE Trans. on Software Engineering\u00a029(4), 524\u2013541 (2003)","journal-title":"IEEE Trans. on Software Engineering"},{"key":"10_CR2","unstructured":"Bialas, J.: The \u03c3-Additive Measure Theory. Journal of Formalized Mathematics\u00a02 (1990)"},{"key":"10_CR3","volume-title":"Model Checking","author":"E.M. Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2000)"},{"key":"10_CR4","volume-title":"Probability and Statistics","author":"M. DeGroot","year":"1989","unstructured":"DeGroot, M.: Probability and Statistics. Addison-Wesley, Reading (1989)"},{"key":"10_CR5","volume-title":"Introduction to Probability","author":"C.M. Grinstead","year":"1997","unstructured":"Grinstead, C.M., Snell, J.L.: Introduction to Probability. American Mathematical Society, Providence, RI (1997)"},{"key":"10_CR6","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4471-1591-5","volume-title":"Theorem Proving with the Real Numbers","author":"J.. Harrison","year":"1998","unstructured":"Harrison, J.: Theorem Proving with the Real Numbers. Springer, Heidelberg (1998)"},{"key":"10_CR7","series-title":"LNAI","first-page":"3","volume-title":"Conference on Automated Deduction","author":"O. Hasan","year":"2007","unstructured":"Hasan, O., Tahar, S.: Formalization of the Continuous Probability Distributions. In: Conference on Automated Deduction. LNCS (LNAI), vol.\u00a04603, pp. 3\u201318. Springer, Heidelberg (2007)"},{"key":"10_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/978-3-540-73210-5_18","volume-title":"Integrated Formal Methods","author":"O. Hasan","year":"2007","unstructured":"Hasan, O., Tahar, S.: Verification of Probabilistic Properties in HOL using the Cumulative Distribution Function. In: Integrated Formal Methods. LNCS, vol.\u00a04591, pp. 333\u2013352. Springer, Heidelberg (2007)"},{"key":"10_CR9","unstructured":"Hurd, J.: Formal Verification of Probabilistic Algorithms. PhD Thesis, University of Cambridge, Cambridge, UK (2002)"},{"key":"10_CR10","unstructured":"Khazanie, R.: Basic Probability Theory and Applications. Goodyear (1976)"},{"issue":"2","key":"10_CR11","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1016\/j.entcs.2005.10.030","volume":"153","author":"M. Kwiatkowska","year":"2005","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Quantitative Analysis with the Probabilistic Model Checker PRISM. Electronic Notes in Theoretical Computer Science\u00a0153(2), 5\u201331 (2005)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"10_CR12","volume-title":"Modern Cryptography: Theory and Practice","author":"W. Mao","year":"2003","unstructured":"Mao, W.: Modern Cryptography: Theory and Practice. Prentice-Hall, Englewood Cliffs (2003)"},{"key":"10_CR13","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511813603","volume-title":"Probability and Computing","author":"M. Mitzenmacher","year":"2005","unstructured":"Mitzenmacher, M., Upfal, E.: Probability and Computing. Cambridge Press, Cambridge (2005)"},{"key":"10_CR14","unstructured":"Nedzusiak, A.: \u03c3-fields and Probability. Journal of Formalized Mathematics\u00a01 (1989)"},{"key":"10_CR15","doi-asserted-by":"crossref","unstructured":"Richter, S.: Formalizing Integration Theory, with an Application to Probabilistic Algorithms. Diploma Thesis, Technische Universit\u00e4t M\u00fcnchen, Department of Informatics, Germany (2003)","DOI":"10.1007\/978-3-540-30142-4_20"},{"key":"10_CR16","series-title":"CRM Monograph Series","doi-asserted-by":"crossref","DOI":"10.1090\/crmm\/023","volume-title":"Mathematical Techniques for Analyzing Concurrent and Probabilisitc Systems","author":"J. Rutten","year":"2004","unstructured":"Rutten, J., Kwaiatkowska, M., Normal, G., Parker, D.: Mathematical Techniques for Analyzing Concurrent and Probabilisitc Systems. CRM Monograph Series, vol.\u00a023. American Mathematical Society, Providence, RI (2004)"},{"key":"10_CR17","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1109\/QEST.2005.42","volume-title":"IEEE International Conference on the Quantitative Evaluation of Systems","author":"K. Sen","year":"2005","unstructured":"Sen, K., Viswanathan, M., Agha, G.: VESTA: A Statistical Model-Checker and Analyzer for Probabilistic Systems. In: IEEE International Conference on the Quantitative Evaluation of Systems, Washington, DC, USA, pp. 251\u2013252. IEEE Computer Soceity Press, Los Alamitos (2005)"},{"key":"10_CR18","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511813658","volume-title":"Probability with Martingales","author":"D. Williams","year":"1991","unstructured":"Williams, D.: Probability with Martingales. Cambridge Press, Cambridge (1991)"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-74591-4_10.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T10:28:04Z","timestamp":1619519284000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-74591-4_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540745907","9783540745914"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-74591-4_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}