{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,11]],"date-time":"2026-05-11T11:19:29Z","timestamp":1778498369754,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642397981","type":"print"},{"value":"9783642397998","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-39799-8_34","type":"book-chapter","created":{"date-parts":[[2013,7,10]],"date-time":"2013-07-10T23:13:06Z","timestamp":1373497986000},"page":"511-526","source":"Crossref","is-referenced-by-count":124,"title":["Probabilistic Program Analysis with Martingales"],"prefix":"10.1007","author":[{"given":"Aleksandar","family":"Chakarov","sequence":"first","affiliation":[]},{"given":"Sriram","family":"Sankaranarayanan","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"1-2","key":"34_CR1","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.scico.2007.08.001","volume":"72","author":"R. Bagnara","year":"2008","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)","journal-title":"Science of Computer Programming"},{"key":"34_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"430","DOI":"10.1007\/3-540-63165-8_199","volume-title":"Proc. ICALP 1997","author":"C. Baier","year":"1997","unstructured":"Baier, C., Clarke, E., Hartonas-Garmhausen, V., Kwiatkowska, M., Ryan, M.: Symbolic model checking for probabilistic processes. In: Degano, P., Gorrieri, R., Marchetti-Spaccamela, A. (eds.) ICALP 1997. LNCS, vol.\u00a01256, pp. 430\u2013440. Springer, Heidelberg (1997)"},{"key":"34_CR3","doi-asserted-by":"crossref","unstructured":"Bouissou, O., Goubault, E., Goubault-Larrecq, J., Putot, S.: A generalization of p-boxes to affine arithmetic. Computing (2012)","DOI":"10.1007\/s00607-011-0182-8"},{"key":"34_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1007\/978-3-540-32033-3_24","volume-title":"Term Rewriting and Applications","author":"O. Bournez","year":"2005","unstructured":"Bournez, O., Garnier, F.: Proving positive almost-sure termination. In: Giesl, J. (ed.) RTA 2005. LNCS, vol.\u00a03467, pp. 323\u2013337. Springer, Heidelberg (2005)"},{"key":"34_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/978-3-540-30579-8_8","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A.R. Bradley","year":"2005","unstructured":"Bradley, A.R., Sipma, H.B., Manna, Z.: Termination of polynomial programs. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 113\u2013129. Springer, Heidelberg (2005)"},{"key":"34_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/978-3-642-01702-5_16","volume-title":"Hardware and Software: Verification and Testing","author":"E. Clarke","year":"2009","unstructured":"Clarke, E., Donz\u00e9, A., Legay, A.: Statistical model checking of mixed-analog circuits with an application to a third order \u0394 \u2212 \u03a3 modulator. In: Chockler, H., Hu, A.J. (eds.) HVC 2008. LNCS, vol.\u00a05394, pp. 149\u2013163. Springer, Heidelberg (2009)"},{"key":"34_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1007\/978-3-540-45069-6_39","volume-title":"Computer Aided Verification","author":"M.A. Col\u00f3n","year":"2003","unstructured":"Col\u00f3n, M.A., Sankaranarayanan, S., Sipma, H.B.: Linear invariant generation using non-linear constraint solving. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 420\u2013432. Springer, Heidelberg (2003)"},{"key":"34_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/3-540-45319-9_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Col\u00f3n","year":"2001","unstructured":"Col\u00f3n, M., Sipma, H.: Synthesis of linear ranking functions. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 67\u201381. Springer, Heidelberg (2001)"},{"key":"34_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-30579-8_1","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P. Cousot","year":"2005","unstructured":"Cousot, P.: Proving program invariance and termination by parametric abstraction, lagrangian relaxation and semidefinite programming. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 1\u201324. Springer, Heidelberg (2005)"},{"key":"34_CR10","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among the variables of a program. In: POPL 19878, pp. 84\u201397 (January 1978)","DOI":"10.1145\/512760.512770"},{"key":"34_CR11","doi-asserted-by":"crossref","unstructured":"Cousot, P., Monerau, M.: Probabilistic abstract interpretation. In: Seidl, H. (ed.) ESOP 2012. LNCS, vol.\u00a07211, pp. 169\u2013193. Springer, Heidelberg (2012)","DOI":"10.1007\/978-3-642-28869-2_9"},{"key":"34_CR12","doi-asserted-by":"crossref","unstructured":"Dubhashi, D., Panconesi, A.: Concentration of Measure for the Analysis of Randomized Algorithms. Cambridge University Press (2009)","DOI":"10.1017\/CBO9780511581274"},{"key":"34_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/978-3-642-31424-7_14","volume-title":"Computer Aided Verification","author":"J. Esparza","year":"2012","unstructured":"Esparza, J., Gaiser, A., Kiefer, S.: Proving termination of probabilistic programs using patterns. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol.\u00a07358, pp. 123\u2013138. Springer, Heidelberg (2012)"},{"issue":"3","key":"34_CR14","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1214\/aoms\/1177728976","volume":"24","author":"F. Foster","year":"1953","unstructured":"Foster, F.: On the stochastic matrices associated with certain queuing processes. Annals Mathematical Statistics\u00a024(3), 355\u2013360 (1953)","journal-title":"Annals Mathematical Statistics"},{"key":"34_CR15","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Srivastava, S., Venkatesan, R.: Program analysis as constraint solving. In: PLDI, pp. 281\u2013292. ACM (2008)","DOI":"10.1145\/1379022.1375616"},{"key":"34_CR16","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":"34_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"390","DOI":"10.1007\/978-3-642-15769-1_24","volume-title":"Static Analysis","author":"J.-P. Katoen","year":"2010","unstructured":"Katoen, J.-P., McIver, A.K., Meinicke, L.A., Morgan, C.C.: Linear-invariant generation for probabilistic programs: In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol.\u00a06337, pp. 390\u2013406. Springer, Heidelberg (2010)"},{"issue":"4","key":"34_CR18","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1145\/1530873.1530882","volume":"36","author":"M. Kwiatkowska","year":"2009","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM: probabilistic model checking for performance and reliability analysis. SIGMETRICS Perf. Eval. Review\u00a036(4), 40\u201345 (2009)","journal-title":"SIGMETRICS Perf. Eval. Review"},{"issue":"1-3","key":"34_CR19","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1016\/j.apal.2007.11.006","volume":"152","author":"R. Lassaigne","year":"2008","unstructured":"Lassaigne, R., Peyronnet, S.: Probabilistic verification and approximation. Annals of Pure and Applied Logic\u00a0152(1-3), 122\u2013131 (2008)","journal-title":"Annals of Pure and Applied Logic"},{"key":"34_CR20","unstructured":"McIver, A., Morgan, C.: Abstraction, Refinement and Proof for Probabilistic Systems. Monographs in Computer Science. Springer (2004)"},{"key":"34_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/11889229_4","volume-title":"Refinement Techniques in Software Engineering","author":"A.K. McIver","year":"2006","unstructured":"McIver, A.K., Morgan, C.: Developing and reasoning about probabilistic programs in pGCL. In: Cavalcanti, A., Sampaio, A., Woodcock, J. (eds.) PSSE 2004. LNCS, vol.\u00a03167, pp. 123\u2013155. Springer, Heidelberg (2006)"},{"key":"34_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/3-540-44978-7_10","volume-title":"Programs as Data Objects","author":"A. Min\u00e9","year":"2001","unstructured":"Min\u00e9, A.: A new numerical abstract domain based on difference-bound matrices. In: Danvy, O., Filinski, A. (eds.) PADO 2001. LNCS, vol.\u00a02053, pp. 155\u2013172. Springer, Heidelberg (2001)"},{"issue":"1-2","key":"34_CR23","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. Sci. Comput. Program.\u00a058(1-2), 179\u2013205 (2005)","journal-title":"Sci. Comput. Program."},{"key":"34_CR24","doi-asserted-by":"crossref","unstructured":"Motwani, R., Raghavan, P.: Randomized Algorithms. Cambridge University Press (1995)","DOI":"10.1017\/CBO9780511814075"},{"key":"34_CR25","doi-asserted-by":"crossref","unstructured":"M\u00fcller-Olm, M., Seidl, H.: Precise interprocedural analysis through linear algebra. In: POPL, pp. 330\u2013341. ACM (2004)","DOI":"10.1145\/982962.964029"},{"issue":"2","key":"34_CR26","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/s10817-008-9103-8","volume":"41","author":"A. Platzer","year":"2008","unstructured":"Platzer, A.: Differential dynamic logic for hybrid systems. J. Autom. Reasoning\u00a041(2), 143\u2013189 (2008)","journal-title":"J. Autom. Reasoning"},{"key":"34_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"446","DOI":"10.1007\/978-3-642-22438-6_34","volume-title":"Automated Deduction \u2013 CADE-23","author":"A. Platzer","year":"2011","unstructured":"Platzer, A.: Stochastic differential dynamic logic for stochastic hybrid programs. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol.\u00a06803, pp. 446\u2013460. Springer, Heidelberg (2011)"},{"key":"34_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/978-3-540-24622-0_20","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A. Podelski","year":"2004","unstructured":"Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol.\u00a02937, pp. 239\u2013251. Springer, Heidelberg (2004)"},{"key":"34_CR29","doi-asserted-by":"crossref","unstructured":"Podelski, A., Rybalchenko, A.: Transition invariants. In: LICS, pp. 32\u201341. IEEE Computer Society (2004)","DOI":"10.1109\/LICS.2004.1319598"},{"key":"34_CR30","doi-asserted-by":"crossref","unstructured":"Rodriguez-Carbonell, E., Kapur, D.: Automatic generation of polynomial loop invariants: Algebraic foundations. In: Proc. ISSAC, Spain (2004)","DOI":"10.1145\/1005285.1005324"},{"key":"34_CR31","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan, S., Sipma, H., Manna, Z.: Non-linear loop invariant generation using Gr\u00f6bner bases. In: POPL, pp. 318\u2013330. ACM Press (2004)","DOI":"10.1145\/982962.964028"},{"key":"34_CR32","unstructured":"Williams, D.: Probability with Martingales (Cambridge Mathematical Textbooks). Cambridge University Press (February 1991)"},{"issue":"9","key":"34_CR33","doi-asserted-by":"publisher","first-page":"1368","DOI":"10.1016\/j.ic.2006.05.002","volume":"204","author":"H.L.S. Younes","year":"2006","unstructured":"Younes, H.L.S., Simmons, R.G.: Statistical probabilitistic model checking with a focus on time-bounded properties. Information & Computation\u00a0204(9), 1368\u20131409 (2006)","journal-title":"Information & Computation"}],"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-39799-8_34","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,15]],"date-time":"2019-05-15T18:28:19Z","timestamp":1557944899000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-39799-8_34"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642397981","9783642397998"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-39799-8_34","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}