{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T03:08:24Z","timestamp":1742958504404,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642237010"},{"type":"electronic","value":"9783642237027"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-23702-7_25","type":"book-chapter","created":{"date-parts":[[2011,9,9]],"date-time":"2011-09-09T17:31:31Z","timestamp":1315589491000},"page":"334-350","source":"Crossref","is-referenced-by-count":6,"title":["Probabilistic Abstractions with Arbitrary Domains"],"prefix":"10.1007","author":[{"given":"Javier","family":"Esparza","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andreas","family":"Gaiser","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"25_CR1","unstructured":"PRISM homepage: http:\/\/www.prismmodelchecker.org\/"},{"key":"25_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/978-3-540-71410-1_16","volume-title":"Logic-Based Program Synthesis and Transformation","author":"R. Bagnara","year":"2007","unstructured":"Bagnara, R., Dobson, K., Hill, P.M., Mundell, M., Zaffanella, E.: Grids: A domain for analyzing the distribution of numerical values. In: Puebla, G. (ed.) LOPSTR 2006. LNCS, vol.\u00a04407, pp. 219\u2013235. Springer, Heidelberg (2007)"},{"key":"25_CR3","doi-asserted-by":"crossref","unstructured":"Bagnara, R., Hill, P.M., Zaffanella, E.: The Parma Polyhedra Library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Science of Computer Programming\u00a072(1-2), 3\u201321 (2008)","DOI":"10.1016\/j.scico.2007.08.001"},{"issue":"5-6","key":"25_CR4","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1007\/s10009-007-0044-z","volume":"9","author":"D. Beyer","year":"2007","unstructured":"Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The software model checker BLAST. Proc. of STTT\u00a09(5-6), 505\u2013525 (2007)","journal-title":"Proc. of STTT"},{"key":"25_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/3-540-36377-7_5","volume-title":"The Essence of Computation","author":"B. Blanchet","year":"2002","unstructured":"Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software. In: Mogensen, T.\u00c6., Schmidt, D.A., Sudborough, I.H. (eds.) The Essence of Computation. LNCS, vol.\u00a02566, pp. 85\u2013108. Springer, Heidelberg (2002)"},{"issue":"2","key":"25_CR6","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1016\/0890-5401(92)90048-K","volume":"96","author":"A. Condon","year":"1992","unstructured":"Condon, A.: The complexity of stochastic games. Inf. Comput.\u00a096(2), 203\u2013224 (1992)","journal-title":"Inf. Comput."},{"key":"25_CR7","doi-asserted-by":"crossref","unstructured":"Condon, A.: On algorithms for simple stochastic games. DIMACS Series in Discr. Math. and Theor. Comp. Sci., vol.\u00a013, pp. 51\u201373. AMS (1993)","DOI":"10.1090\/dimacs\/013\/04"},{"key":"25_CR8","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proc. of POPL, pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"25_CR9","first-page":"269","volume-title":"POPL","author":"P. Cousot","year":"1979","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: POPL, San Antonio, Texas, pp. 269\u2013282. ACM Press, New York (1979)"},{"key":"25_CR10","unstructured":"Esparza, J., Gaiser, A.: Probabilistic abstractions with arbitrary domains. Technical report, Technische Universit\u00e4t M\u00fcnchen (2011), http:\/\/arxiv.org\/abs\/1106.1364"},{"key":"25_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1007\/978-3-540-78800-3_33","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"B.S. Gulavani","year":"2008","unstructured":"Gulavani, B.S., Chakraborty, S., Nori, A.V., Rajamani, S.K.: Automatically refining abstract interpretations. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 443\u2013458. Springer, Heidelberg (2008)"},{"key":"25_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"474","DOI":"10.1007\/11691372_34","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"B.S. Gulavani","year":"2006","unstructured":"Gulavani, B.S., Rajamani, S.K.: Counterexample driven refinement for abstract interpretation. In: Hermanns, H. (ed.) TACAS 2006. LNCS, vol.\u00a03920, pp. 474\u2013488. Springer, Heidelberg (2006)"},{"key":"25_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/978-3-642-12002-2_30","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E.M. Hahn","year":"2010","unstructured":"Hahn, E.M., Hermanns, H., Wachter, B., Zhang, L.: PASS: Abstraction refinement for infinite probabilistic models. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol.\u00a06015, pp. 353\u2013357. Springer, Heidelberg (2010)"},{"key":"25_CR14","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":"25_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"661","DOI":"10.1007\/978-3-642-02658-4_52","volume-title":"Computer Aided Verification","author":"B. Jeannet","year":"2009","unstructured":"Jeannet, B., Min\u00e9, A.: apron: A library of numerical abstract domains for static analysis. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 661\u2013667. Springer, Heidelberg (2009)"},{"key":"25_CR16","doi-asserted-by":"crossref","unstructured":"Kattenbelt, M., Kwiatkowska, M.Z., Norman, G., Parker, D.: Abstraction refinement for probabilistic software. In: Jones, N.D., M\u00fcller-Olm, M. (eds.) VMCAI 2009. LNCS, vol.\u00a05403, pp. 182\u2013197. Springer, Heidelberg (2009)","DOI":"10.1007\/978-3-540-93900-9_17"},{"key":"25_CR17","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/s10703-010-0097-6","volume":"36","author":"M. Kattenbelt","year":"2010","unstructured":"Kattenbelt, M., Kwiatkowska, M.Z., Norman, G., Parker, D.: A game-based abstraction-refinement framework for markov decision processes. Form. Methods Syst. Des.\u00a036, 246\u2013280 (2010)","journal-title":"Form. Methods Syst. Des."},{"key":"25_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"322","DOI":"10.1007\/978-3-540-45099-3_17","volume-title":"Static Analysis","author":"D. Monniaux","year":"2000","unstructured":"Monniaux, D.: Abstract interpretation of probabilistic semantics. In: SAS 2000. LNCS, vol.\u00a01824, pp. 322\u2013340. Springer, Heidelberg (2000)"},{"key":"25_CR19","doi-asserted-by":"crossref","unstructured":"Monniaux, D.: Abstract interpretation of programs as markov decision processes. In: Proc. of SAS, pp. 237\u2013254 (2003)","DOI":"10.1007\/3-540-44898-5_13"},{"issue":"3","key":"25_CR20","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1016\/j.entcs.2007.07.005","volume":"190","author":"A. Pierro Di","year":"2007","unstructured":"Di Pierro, A., Hankin, C., Wiklicky, H.: On probabilistic techniques for data flow analysis. Electr. Notes Theor. Comput. Sci.\u00a0190(3), 59\u201377 (2007)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"25_CR21","doi-asserted-by":"publisher","DOI":"10.1002\/9780470316887","volume-title":"Markov Decision Processes: Discrete Stochastic Dynamic Programming","author":"M.L. Puterman","year":"1994","unstructured":"Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley Interscience, Hoboken (1994)"},{"key":"25_CR22","unstructured":"Wachter, B.: Refined Probabilistic Abstraction. PhD thesis, Universit\u00e4t des Saarlandes (2011)"},{"key":"25_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"362","DOI":"10.1007\/978-3-642-11319-2_26","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"B. Wachter","year":"2010","unstructured":"Wachter, B., Zhang, L.: Best probabilistic transformers. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol.\u00a05944, pp. 362\u2013379. Springer, Heidelberg (2010)"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-23702-7_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,15]],"date-time":"2019-06-15T03:03:32Z","timestamp":1560567812000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-23702-7_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642237010","9783642237027"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-23702-7_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}