{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:09:51Z","timestamp":1760202591274},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540938996"},{"type":"electronic","value":"9783540939009"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1007\/978-3-540-93900-9_17","type":"book-chapter","created":{"date-parts":[[2008,12,15]],"date-time":"2008-12-15T09:35:59Z","timestamp":1229333759000},"page":"182-197","source":"Crossref","is-referenced-by-count":34,"title":["Abstraction Refinement for Probabilistic Software"],"prefix":"10.1007","author":[{"given":"Mark","family":"Kattenbelt","sequence":"first","affiliation":[]},{"given":"Marta","family":"Kwiatkowska","sequence":"additional","affiliation":[]},{"given":"Gethin","family":"Norman","sequence":"additional","affiliation":[]},{"given":"David","family":"Parker","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"17_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 72\u201383. Springer, Heidelberg (1997)"},{"key":"17_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E. Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 154\u2013169. Springer, Heidelberg (2000)"},{"key":"17_CR3","first-page":"157","volume-title":"Proc. QEST 2006","author":"M. Kwiatkowska","year":"2006","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Game-based abstraction for Markov decision processes. In: Proc. QEST 2006, pp. 157\u2013166. IEEE, Los Alamitos (2006)"},{"issue":"2-3","key":"17_CR4","first-page":"105","volume":"25","author":"E. Clarke","year":"2004","unstructured":"Clarke, E., Kroening, D., Sharygina, N., Yorav, K.: Predicate abstraction of ANSI-C programs using SAT. FMSD\u00a025(2-3), 105\u2013127 (2004)","journal-title":"FMSD"},{"key":"17_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/978-3-540-70545-1_16","volume-title":"Computer Aided Verification","author":"H. Hermanns","year":"2008","unstructured":"Hermanns, H., Wachter, B., Zhang, L.: Probabilistic CEGAR. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 162\u2013175. Springer, Heidelberg (2008)"},{"key":"17_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/3-540-44804-7_3","volume-title":"Process Algebra and Probabilistic Methods. Performance Modelling and Verification","author":"P. D\u2019Argenio","year":"2001","unstructured":"D\u2019Argenio, P., Jeannet, B., Jensen, H., Larsen, K.: Reachability analysis of probabilistic systems by successive refinements. In: de Luca, L., Gilmore, S. (eds.) PROBMIV 2001, PAPM-PROBMIV 2001, and PAPM 2001. LNCS, vol.\u00a02165, pp. 39\u201356. Springer, Heidelberg (2001)"},{"key":"17_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/978-3-540-71209-1_8","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T. Han","year":"2007","unstructured":"Han, T., Katoen, J.-P.: Counterexamples in probabilistic model checking. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 72\u201386. Springer, Heidelberg (2007)"},{"key":"17_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/978-3-540-73368-3_38","volume-title":"Computer Aided Verification","author":"L. Alfaro de","year":"2007","unstructured":"de Alfaro, L., Roy, P.: Magnifying-lens abstraction for Markov decision processes. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 325\u2013338. Springer, Heidelberg (2007)"},{"key":"17_CR9","volume-title":"Proc. QEST 2008","author":"P. Roy","year":"2008","unstructured":"Roy, P., Parker, D., Norman, G., de Alfaro, L.: Symbolic magnifying lens abstraction in Markov decision processes. In: Proc. QEST 2008. IEEE, Los Alamitos (2008)"},{"key":"17_CR10","unstructured":"Chatterjee, K., Henzinger, T., Jhala, R., Majumdar, R.: Counterexample-guided planning. In: Proc. UAI 2005, pp. 104\u2013111 (2005)"},{"key":"17_CR11","volume-title":"Abstraction, refinement and proof for probabilistic systems","author":"A. McIver","year":"2004","unstructured":"McIver, A., Morgan, C.: Abstraction, refinement and proof for probabilistic systems. Springer, Heidelberg (2004)"},{"issue":"1","key":"17_CR12","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1016\/j.tcs.2005.08.008","volume":"346","author":"M. Huth","year":"2005","unstructured":"Huth, M.: On finite-state approximants for probabilistic computation tree logic. Theoretical Computer Science\u00a0346(1), 113\u2013134 (2005)","journal-title":"Theoretical Computer Science"},{"key":"17_CR13","doi-asserted-by":"crossref","unstructured":"Kattenbelt, M., Kwiatkowska, M., Norman, G., Parker, D.: Game-based probabilistic predicate abstraction in PRISM. In: Proc. QAPL 2008(2008)","DOI":"10.1016\/j.entcs.2008.11.016"},{"key":"17_CR14","first-page":"127","volume-title":"Proc. PPDP 2000","author":"A.D. Pierro","year":"2000","unstructured":"Pierro, A.D., Wiklicky, H.: Concurrent constraint programming: Towards probabilistic abstract interpretation. In: Proc. PPDP 2000, pp. 127\u2013138. ACM Press, New York (2000)"},{"issue":"1-2","key":"17_CR15","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1016\/j.scico.2005.02.008","volume":"58","author":"D. Monniaux","year":"2005","unstructured":"Monniaux, D.: Abstract interpretation of programs as Markov decision processes. Science of Computer Programming\u00a058(1-2), 179\u2013205 (2005)","journal-title":"Science of Computer Programming"},{"key":"17_CR16","doi-asserted-by":"crossref","unstructured":"Smith, M.: Probabilistic abstract interpretation of imperative programs using truncated normal distributions. In: Proc. QAPL 2008 (2008)","DOI":"10.1016\/j.entcs.2008.11.018"},{"key":"17_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-540-78800-3_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Legay","year":"2008","unstructured":"Legay, A., Murawski, A., Ouaknine, J., Worrell, J.: On automated verification of probabilistic programs. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 173\u2013187. Springer, Heidelberg (2008)"},{"key":"17_CR18","first-page":"131","volume-title":"Proc. QEST 2006","author":"F. Ciesinski","year":"2006","unstructured":"Ciesinski, F., Baier, C.: Liquor: A tool for qualitative and quantitative linear time analysis of reactive systems. In: Proc. QEST 2006, pp. 131\u2013132. IEEE, Los Alamitos (2006)"},{"key":"17_CR19","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4684-9455-6","volume-title":"Denumerable Markov Chains","author":"J. Kemeny","year":"1976","unstructured":"Kemeny, J., Snell, J., Knapp, A.: Denumerable Markov Chains, 2nd edn. Springer, Heidelberg (1976)","edition":"2"},{"key":"17_CR20","doi-asserted-by":"publisher","first-page":"1095","DOI":"10.1073\/pnas.39.10.1953","volume":"39","author":"L. Shapley","year":"1953","unstructured":"Shapley, L.: Stochastic games. Proc. Nat. Acad. Science\u00a039, 1095\u20131100 (1953)","journal-title":"Proc. Nat. Acad. Science"},{"key":"17_CR21","unstructured":"de Alfaro, L.: Formal Verification of Probabilistic Systems. PhD thesis (1997)"},{"key":"17_CR22","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1090\/dimacs\/013\/04","volume":"13","author":"A. Condon","year":"1993","unstructured":"Condon, A.: On algorithms for simple stochastic games. Advances in computational complexity theory\u00a013, 51\u201373 (1993)","journal-title":"Advances in computational complexity theory"},{"key":"17_CR23","unstructured":"GOTO-CC, \n                    \n                      http:\/\/www.verify.ethz.ch\/goto-cc\/"},{"key":"17_CR24","doi-asserted-by":"crossref","unstructured":"Ball, T., Majumdar, R., Millstein, T., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: Proc. PLDI 2001, pp. 203\u2013213 (2001)","DOI":"10.1145\/378795.378846"},{"issue":"5","key":"17_CR25","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"E. Clarke","year":"1994","unstructured":"Clarke, E., Grumberg, O., Long, D.: Model checking and abstraction. ACM Trans. Program. Lang. Syst.\u00a016(5), 1512\u20131542 (1994)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"17_CR26","unstructured":"Kattenbelt, M., Kwiatkowska, M., Norman, G., Parker, D.: A game-based abstraction-refinement framework for Markov decision processes. Technical Report RR-08-06, Oxford University Computing Laboratory (2008)"},{"key":"17_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"459","DOI":"10.1007\/11691372_33","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Jhala","year":"2006","unstructured":"Jhala, R., McMillan, K.: A practical and complete approach to predicate refinement. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol.\u00a03920, pp. 459\u2013473. Springer, Heidelberg (2006)"},{"key":"17_CR28","first-page":"232","volume-title":"Proc. POPL 2004","author":"T. Henzinger","year":"2004","unstructured":"Henzinger, T., Jhala, R., Majumdar, R., McMillan, K.: Abstractions from proofs. In: Proc. POPL 2004, pp. 232\u2013244. ACM Press, New York (2004)"},{"key":"17_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"382","DOI":"10.1007\/978-3-540-31980-1_40","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Clarke","year":"2005","unstructured":"Clarke, E., Kroening, D., Sharygina, N., Yorav, K.: SATABS: SAT-based predicate abstraction for ANSI-C. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 382\u2013396. Springer, Heidelberg (2005)"},{"key":"17_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/11691372_29","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Hinton","year":"2006","unstructured":"Hinton, A., Kwiatkowska, M., Norman, G., Parker, D.: PRISM: A tool for automatic verification of probabilistic systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol.\u00a03920, pp. 441\u2013444. Springer, Heidelberg (2006)"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-93900-9_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,1,25]],"date-time":"2019-01-25T09:27:55Z","timestamp":1548408475000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-93900-9_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540938996","9783540939009"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-93900-9_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}