{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T08:44:15Z","timestamp":1770281055227,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540668565","type":"print"},{"value":"9783540466741","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-46674-6_11","type":"book-chapter","created":{"date-parts":[[2007,11,29]],"date-time":"2007-11-29T15:50:17Z","timestamp":1196351417000},"page":"113-125","source":"Crossref","is-referenced-by-count":9,"title":["Verifying Probabilistic Programs Using a Hoare like Logic"],"prefix":"10.1007","author":[{"given":"J. I.","family":"den Hartog","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[1999,11,19]]},"reference":[{"key":"11_CR1","unstructured":"L. de Alfaro. Formal Verification of Probabilistic Systems. PhD thesis, Stanford University, 1997."},{"key":"11_CR2","unstructured":"S. Andova. Probabilistic process algebra. In Proceedings of ARTS\u201999, Bamberg, Germany, 1999."},{"key":"11_CR3","doi-asserted-by":"crossref","unstructured":"K.R. Apt and E.-R. Olderog. Verification of Sequential and Concurrent Programs. Texts and Monographs in Computer Science. Springer-Verlag, 1991.","DOI":"10.1007\/978-1-4757-4376-0"},{"key":"11_CR4","unstructured":"C. Baier, M. Kwiatkowska, and G. Norman. Computing probabilistic lower and upper bounds for ltl formulae over sequential and concurrent markov chains. Technical Report CSR-98-4, University of Birmingham, June 1998."},{"key":"11_CR5","unstructured":"J.W. de Bakker. Mathematical Theory of Program Correctness. Series in Computer Science. Prentice-Hall Internationall, 1980."},{"key":"11_CR6","unstructured":"P.R. D\u2019Argenio, J.-P. Katoen, and E. Brinksma. A stochastic process algebra for discrete event simulation. Technical report, University of Twente, 1998."},{"key":"11_CR7","unstructured":"N. Francez. Program Verification. International Computer Science Series. Addison-Wesley, 1992."},{"key":"11_CR8","unstructured":"J.I. den Hartog. Comparative semantics for a process language with probabilistic choice and non-determinism. Technical Report IR-445, Vrije Universiteit, Ams-terdam, February 1998."},{"key":"11_CR9","doi-asserted-by":"crossref","unstructured":"J.I. den Hartog and E.P. de Vink. Mixing up nondeterminism and probability: A preliminary report. ENTCS, 1999. to appear.","DOI":"10.1016\/S1571-0661(05)82521-6"},{"key":"11_CR10","unstructured":"J.I. den Hartog and E.P. de Vink. Taking chances on merge and fail: Extending strong and probabilistic bisimulation. Technical Report IR-454, Vrije Universiteit, Amsterdam, March 1999."},{"key":"11_CR11","unstructured":"H. Hermanns. Interactive Markov Chains. PhD thesis, University of Erlangen-Nurnberg, July 1998."},{"key":"11_CR12","unstructured":"J. Hooman. Program design in PVS. In Proceedings Workshop on Tool Support for System Development and Verification, June 1996."},{"key":"11_CR13","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1016\/0022-0000(85)90012-1","volume":"30","author":"D. Kozen","year":"1985","unstructured":"D. Kozen. A probabilistic PDL. Journal of Computer and System Sciences, 30:162\u2013178, 1985.","journal-title":"Journal of Computer and System Sciences"},{"key":"11_CR14","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(91)90030-6","volume":"94","author":"K.G. Larsen","year":"1991","unstructured":"K.G. Larsen and A. Skou. Bisimulation through probabilistic testing. Information and Computation, 94:1\u201328, 1991.","journal-title":"Information and Computation"},{"key":"11_CR15","unstructured":"N. Lynch. Distributed Algorithms. The Morgan Kaufmann series in data manage-ment systems. Kaufmann, 1996."},{"key":"11_CR16","unstructured":"C. Morgan and A. McIver. pGCL: formal reasoning for random algorithms. South African Computer Journal, 1999. to appear."},{"issue":"3","key":"11_CR17","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1145\/229542.229547","volume":"18","author":"C. Morgan","year":"1996","unstructured":"C. Morgan, A. McIver, and K. Seidel. Probabilistic predicate transformers. ACM Transactions on Programming Languages and Systems, 18(3):325\u2013353, May 1996.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"11_CR18","doi-asserted-by":"crossref","unstructured":"R. Motwani and P. Raghavan. Randomized Algorithms. Cambridge University Press, 1995.","DOI":"10.1017\/CBO9780511814075"},{"key":"11_CR19","unstructured":"R. Segala. Modeling and Verification of Randomized Distributed Real-Time Systems. PhD thesis, Massachusetts Institute of Technology, June 1995."},{"key":"11_CR20","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S0304-3975(97)00056-X","volume":"176","author":"S.-H. Wu","year":"1999","unstructured":"S.-H. Wu, S.A. Smolka, and E.W. Stark. Composition and behavior of probabilistic I\/O automata. Theoretical Computer Science, 176:1\u201338, 1999.","journal-title":"Theoretical Computer Science"}],"container-title":["Lecture Notes in Computer Science","Advances in Computing Science \u2014 ASIAN\u201999"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-46674-6_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,15]],"date-time":"2023-05-15T00:47:28Z","timestamp":1684111648000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-46674-6_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540668565","9783540466741"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/3-540-46674-6_11","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[1999]]}}}