{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:57:03Z","timestamp":1776333423071,"version":"3.51.2"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642314230","type":"print"},{"value":"9783642314247","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-31424-7_25","type":"book-chapter","created":{"date-parts":[[2012,6,21]],"date-time":"2012-06-21T10:26:49Z","timestamp":1340274409000},"page":"310-326","source":"Crossref","is-referenced-by-count":35,"title":["Assume-Guarantee Abstraction Refinement for Probabilistic Systems"],"prefix":"10.1007","author":[{"given":"Anvesh","family":"Komuravelli","sequence":"first","affiliation":[]},{"given":"Corina S.","family":"P\u0103s\u0103reanu","sequence":"additional","affiliation":[]},{"given":"Edmund M.","family":"Clarke","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"25_CR1","unstructured":"Baier, C.: On Algorithmic Verification Methods for Probabilistic Systems. Habilitation thesis, Fakult\u00e4t f\u00fcr Mathematik und Informatik, Univ. Mannheim (1998)"},{"key":"25_CR2","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"issue":"1","key":"25_CR3","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1838552.1838553","volume":"12","author":"R. Chadha","year":"2010","unstructured":"Chadha, R., Viswanathan, M.: A Counterexample-Guided Abstraction-Refinement Framework for Markov Decision Processes. TOCL\u00a012(1), 1\u201349 (2010)","journal-title":"TOCL"},{"key":"25_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"534","DOI":"10.1007\/11513988_51","volume-title":"Computer Aided Verification","author":"S. Chaki","year":"2005","unstructured":"Chaki, S., Clarke, E., Sinha, N., Thati, P.: Automated Assume-Guarantee Reasoning for Simulation Conformance. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 534\u2013547. Springer, Heidelberg (2005)"},{"key":"25_CR5","unstructured":"Chaki, S.J.: A Counterexample Guided Abstraction Refinement Framework for Verifying Concurrent C Programs. PhD thesis, Carnegie Mellon University (2005)"},{"key":"25_CR6","doi-asserted-by":"crossref","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)","DOI":"10.1007\/10722167_15"},{"key":"25_CR7","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":"25_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1007\/3-540-44685-0_24","volume-title":"CONCUR 2001 - Concurrency Theory","author":"L. Alfaro de","year":"2001","unstructured":"de Alfaro, L., Henzinger, T.A., Jhala, R.: Compositional Methods for Probabilistic Systems. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol.\u00a02154, pp. 351\u2013365. Springer, Heidelberg (2001)"},{"key":"25_CR9","unstructured":"Dutertre, B., Moura, L.D.: The Yices SMT Solver. Technical report, SRI International (2006)"},{"key":"25_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1007\/978-3-642-24372-1_40","volume-title":"Automated Technology for Verification and Analysis","author":"L. Feng","year":"2011","unstructured":"Feng, L., Han, T., Kwiatkowska, M., Parker, D.: Learning-Based Compositional Verification for Synchronous Probabilistic Systems. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol.\u00a06996, pp. 511\u2013521. Springer, Heidelberg (2011)"},{"key":"25_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-642-19811-3_2","volume-title":"Fundamental Approaches to Software Engineering","author":"L. Feng","year":"2011","unstructured":"Feng, L., Kwiatkowska, M., Parker, D.: Automated Learning of Probabilistic Assumptions for Compositional Reasoning. In: Giannakopoulou, D., Orejas, F. (eds.) FASE 2011. LNCS, vol.\u00a06603, pp. 2\u201317. Springer, Heidelberg (2011)"},{"key":"25_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-540-70545-1_14","volume-title":"Computer Aided Verification","author":"M. Gheorghiu Bobaru","year":"2008","unstructured":"Gheorghiu Bobaru, M., P\u0103s\u0103reanu, C.S., Giannakopoulou, D.: Automated Assume-Guarantee Reasoning by Abstraction Refinement. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 135\u2013148. Springer, Heidelberg (2008)"},{"key":"25_CR13","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_CR14","unstructured":"Komuravelli, A., P\u0103s\u0103reanu, C.S., Clarke, E.M.: Learning Probabilistic Systems from Tree Samples. In: LICS (to appear, 2012)"},{"key":"25_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M. Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: Verification of Probabilistic Real-Time Systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 585\u2013591. Springer, Heidelberg (2011)"},{"key":"25_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-642-12002-2_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Kwiatkowska","year":"2010","unstructured":"Kwiatkowska, M., Norman, G., Parker, D., Qu, H.: Assume-Guarantee Verification for Probabilistic Systems. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol.\u00a06015, pp. 23\u201337. Springer, Heidelberg (2010)"},{"key":"25_CR17","unstructured":"Milner, R.: An Algebraic Definition of Simulation between Programs. Technical report, Stanford University (1971)"},{"key":"25_CR18","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: In Transition from Global to Modular Temporal Reasoning about Programs. In: LMCS. NATO ASI, vol.\u00a013, pp. 123\u2013144. Springer (1985)","DOI":"10.1007\/978-3-642-82453-1_5"},{"issue":"3","key":"25_CR19","first-page":"175","volume":"32","author":"C.S. P\u0103s\u0103reanu","year":"2008","unstructured":"P\u0103s\u0103reanu, C.S., Giannakopoulou, D., Bobaru, M.G., Cobleigh, J.M., Barringer, H.: Learning to Divide and Conquer: Applying the L* Algorithm to Automate Assume-Guarantee Reasoning. FMSD\u00a032(3), 175\u2013205 (2008)","journal-title":"FMSD"},{"issue":"2","key":"25_CR20","first-page":"250","volume":"2","author":"R. Segala","year":"1995","unstructured":"Segala, R., Lynch, N.: Probabilistic Simulations for Probabilistic Processes. Nordic J. of Computing\u00a02(2), 250\u2013273 (1995)","journal-title":"Nordic J. of Computing"},{"key":"25_CR21","unstructured":"Zhang, L.: Decision Algorithms for Probabilistic Simulations. PhD thesis, Universit\u00e4t des Saarlandes (2008)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-31424-7_25.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T07:59:53Z","timestamp":1620115193000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-31424-7_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642314230","9783642314247"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-31424-7_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}