{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:01:01Z","timestamp":1725490861831},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540735946"},{"type":"electronic","value":"9783540735953"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73595-3_2","type":"book-chapter","created":{"date-parts":[[2007,8,30]],"date-time":"2007-08-30T05:31:33Z","timestamp":1188451893000},"page":"3-18","source":"Crossref","is-referenced-by-count":15,"title":["Formalization of Continuous Probability Distributions"],"prefix":"10.1007","author":[{"given":"Osman","family":"Hasan","sequence":"first","affiliation":[]},{"given":"Sofi\u00e8ne","family":"Tahar","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"1-2","key":"2_CR1","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/s10703-005-2256-8","volume":"27","author":"B. Akbarpour","year":"2005","unstructured":"Akbarpour, B., Tahar, S.: Formalization of Fixed-Point Arithmetic in HOL. Formal Methods in Systems Design\u00a027(1-2), 173\u2013200 (2005)","journal-title":"Formal Methods in Systems Design"},{"key":"2_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/11783596_6","volume-title":"Mathematics of Program Construction","author":"P. Audebaud","year":"2006","unstructured":"Audebaud, P., Paulin-Mohring, C.: Proofs of Randomized Algorithms in Coq. In: Uustalu, T. (ed.) MPC 2006. LNCS, vol.\u00a04014, pp. 49\u201368. Springer, Heidelberg (2006)"},{"issue":"4","key":"2_CR3","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":"2_CR4","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":"2_CR5","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4613-8643-8","volume-title":"Non-Uniform Random Variate Generation","author":"L. Devroye","year":"1986","unstructured":"Devroye, L.: Non-Uniform Random Variate Generation. Springer, Heidelberg (1986)"},{"issue":"4","key":"2_CR6","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1109\/26.2768","volume":"36","author":"T.A. Gonsalves","year":"1988","unstructured":"Gonsalves, T.A, Tobagi, F.A: On the Performance Effects of Station Locations and Access Protocol Parameters in Ethernet Networks. IEEE Trans. on Communications\u00a036(4), 441\u2013449 (1988)","journal-title":"IEEE Trans. on Communications"},{"key":"2_CR7","doi-asserted-by":"crossref","first-page":"387","DOI":"10.1007\/978-1-4612-3658-0_10","volume-title":"Current Trends in Hardware Verification and Automated Theorem Proving","author":"M.J.C. Gordon","year":"1989","unstructured":"Gordon, M.J.C: Mechanizing Programming Logics in Higher-0rder Logic. In: Current Trends in Hardware Verification and Automated Theorem Proving, pp. 387\u2013439. Springer, Heidelberg (1989)"},{"key":"2_CR8","volume-title":"Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic","author":"M.J.C. Gordon","year":"1993","unstructured":"Gordon, M.J.C, Melham, T.F: Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic. Cambridge University Press, Cambridge (1993)"},{"key":"2_CR9","first-page":"189","volume-title":"Principles of Programming Languages","author":"V.T. Gupta","year":"1999","unstructured":"Gupta, V.T, Jagadeesan, R., Panangaden, P.: Stochastic Processes as Concurrent Constraint Programs. In: Principles of Programming Languages, pp. 189\u2013202. ACM Press, New York (1999)"},{"key":"2_CR10","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":"2_CR11","doi-asserted-by":"crossref","unstructured":"Hasan, O., Tahar, S.: Formalization of the Standard Uniform Random Variable. Theoretical Computer Science (to appear)","DOI":"10.1016\/j.tcs.2007.05.009"},{"key":"2_CR12","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":"2_CR13","unstructured":"Hasan, O., Tahar, S.: Formalization of Continuous Probability Distributions. Technical Report, Concordia University, Montreal, Canada (February 2007), \n                    \n                      http:\/\/hvg.ece.concordia.ca\/Publications\/TECH_REP\/FCPD_TR07"},{"key":"2_CR14","unstructured":"Hurd, J.: Formal Verification of Probabilistic Algorithms. PhD Thesis, University of Cambridge, Cambridge, UK (2002)"},{"issue":"3","key":"2_CR15","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1145\/321765.321771","volume":"20","author":"T. Kaneko","year":"1973","unstructured":"Kaneko, T., Liu, B.: On Local Roundoff Errors in Floating-Point Arithmetic. ACM\u00a020(3), 391\u2013398 (1973)","journal-title":"ACM"},{"key":"2_CR16","unstructured":"Khazanie, R.: Basic Probability Theory and Applications. Goodyear (1976)"},{"key":"2_CR17","unstructured":"K\u00f6psel, A., Ebert, J., Wolisz, A.: A Performance Comparison of Point and Distributed Coordination Function of an IEEE 802.11 WLAN in the Presence of Real-Time Requirements. In: Proceedings of Seventh International Workshop on Mobile Multimedia Communications, Tokyo, Japan (2000)"},{"key":"2_CR18","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 University Press, Cambridge (2005)"},{"key":"2_CR19","first-page":"171","volume-title":"Principles of Programming Languages","author":"S. Park","year":"2005","unstructured":"Park, S., Pfenning, F., Thrun, S.: A Probabilistic Language based upon Sampling Functions. In: Principles of Programming Languages, pp. 171\u2013182. ACM Press, New York (2005)"},{"key":"2_CR20","first-page":"733","volume-title":"International Joint Conferences on Artificial Intelligence","author":"A. Pfeffer","year":"2001","unstructured":"Pfeffer, A.: IBAL: A Probabilistic Rational Programming Language. In: International Joint Conferences on Artificial Intelligence, pp. 733\u2013740. Morgan Kaufmann Publishers, Washington (2001)"},{"key":"2_CR21","volume-title":"Simulation","author":"S.M. Ross","year":"2002","unstructured":"Ross, S.M: Simulation. Academic Press, San Diego (2002)"},{"key":"2_CR22","doi-asserted-by":"crossref","unstructured":"Rutten, J., Kwaiatkowska, M., Normal, G., Parker, D.: Mathematical Techniques for Analyzing Concurrent and Probabilisitc Systems. CRM Monograph Series. American Mathematical Society, vol. 23 (2004)","DOI":"10.1090\/crmm\/023"},{"key":"2_CR23","volume-title":"Probability and Statistics with Reliability, Queuing and Computer Science Applications","author":"K.S. Tridevi","year":"2002","unstructured":"Tridevi, K.S: Probability and Statistics with Reliability, Queuing and Computer Science Applications. Wiley, Chichester (2002)"},{"key":"2_CR24","first-page":"555","volume":"81","author":"B. Widrow","year":"1961","unstructured":"Widrow, B.: Statistical Analysis of Amplitude-quantized Sampled Data Systems. AIEE Trans. (Applications and Industry)\u00a081, 555\u2013568 (1961)","journal-title":"AIEE Trans. (Applications and Industry)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-21"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73595-3_2.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T05:53:03Z","timestamp":1619502783000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73595-3_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540735946","9783540735953"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73595-3_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}