{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:16:38Z","timestamp":1763468198419},"publisher-location":"Cham","reference-count":24,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319109350"},{"type":"electronic","value":"9783319109367"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-10936-7_6","type":"book-chapter","created":{"date-parts":[[2014,9,6]],"date-time":"2014-09-06T15:17:55Z","timestamp":1410016675000},"page":"85-100","source":"Crossref","is-referenced-by-count":38,"title":["Expectation Invariants for Probabilistic Program Loops as Fixed Points"],"prefix":"10.1007","author":[{"given":"Aleksandar","family":"Chakarov","sequence":"first","affiliation":[]},{"given":"Sriram","family":"Sankaranarayanan","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"6_CR1","doi-asserted-by":"crossref","unstructured":"Antonopoulos, T., Gorogiannis, N., Haase, C., Kanovich, M., Ouaknine, J.: Foundations for decision problems in separation logic with general inductive predicates. In: Muscholl, A. (ed.) FOSSACS 2014. LNCS, vol.\u00a08412, pp. 411\u2013425. Springer, Heidelberg (2014)","DOI":"10.1007\/978-3-642-54830-7_27"},{"issue":"2-4","key":"6_CR2","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/s00607-011-0182-8","volume":"94","author":"O. Bouissou","year":"2012","unstructured":"Bouissou, O., Goubault, E., Goubault-Larrecq, J., Putot, S.: A generalization of p-boxes to affine arithmetic. Computing\u00a094(2-4), 189\u2013201 (2012)","journal-title":"Computing"},{"key":"6_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1007\/978-3-642-39799-8_34","volume-title":"Computer Aided Verification","author":"A. Chakarov","year":"2013","unstructured":"Chakarov, A., Sankaranarayanan, S.: Probabilistic program analysis with martingales. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol.\u00a08044, pp. 511\u2013526. Springer, Heidelberg (2013)"},{"key":"6_CR4","doi-asserted-by":"crossref","unstructured":"Chakarov, A., Sankaranarayanan, S.: Expectation invaraiants for probabilistic program loops as fixed points (2014) (extended version) (Draft, Available upon request)","DOI":"10.1007\/978-3-319-10936-7_6"},{"key":"6_CR5","volume-title":"A course in probability theory","author":"K.L. Chung","year":"1974","unstructured":"Chung, K.L.: A course in probability theory, vol.\u00a03. Academic Press, New York (1974)"},{"key":"6_CR6","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":"6_CR7","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: ACM Principles of Programming Languages, pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"6_CR8","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among the variables of a program. In: POPL 1978, pp. 84\u201397 (January 1978)","DOI":"10.1145\/512760.512770"},{"key":"6_CR9","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":"6_CR10","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":"6_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/978-3-642-40196-1_17","volume-title":"Quantitative Evaluation of Systems","author":"F. Gretz","year":"2013","unstructured":"Gretz, F., Katoen, J.-P., McIver, A.: Prinsys - on a quest for probabilistic loop invariants. In: Joshi, K., Siegle, M., Stoelinga, M., D\u2019Argenio, P.R. (eds.) QEST 2013. LNCS, vol.\u00a08054, pp. 193\u2013208. Springer, Heidelberg (2013)"},{"key":"6_CR12","unstructured":"Halbwachs, N.: D\u00e9termination automatique de relations lin\u00e9aires v\u00e9rifi\u00e9es par les variables d\u2019un programme. PhD thesis, Institut National Polytechnique de Grenoble-INPG (1979)"},{"key":"6_CR13","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":"3","key":"6_CR14","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1016\/0022-0000(81)90036-2","volume":"22","author":"D. Kozen","year":"1981","unstructured":"Kozen, D.: Semantics of probabilistic programs. J. Comput. Syst. Sci.\u00a022(3), 328\u2013350 (1981)","journal-title":"J. Comput. Syst. Sci."},{"key":"6_CR15","doi-asserted-by":"crossref","unstructured":"Mardziel, P., Magill, S., Hicks, M., Srivatsa, M.: Dynamic enforcement of knowledge-based security policies. In: 2011 IEEE 24th Computer Security Foundations Symposium (CSF), pp. 114\u2013128. IEEE (2011)","DOI":"10.1109\/CSF.2011.15"},{"issue":"2","key":"6_CR16","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1016\/S0168-9525(98)01659-X","volume":"15","author":"H. McAdams","year":"1999","unstructured":"McAdams, H., Arkin, A.: It\u2019s a noisy business! genetic regulation at the nanomolar scale. Trends Genetics\u00a015(2), 65\u201369 (1999)","journal-title":"Trends Genetics"},{"key":"6_CR17","unstructured":"McIver, A., Morgan, C.: Abstraction, Refinement and Proof for Probabilistic Systems. Monographs in Computer Science. Springer (2004)"},{"key":"6_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":"6_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/3-540-45309-1_24","volume-title":"Programming Languages and Systems","author":"D. Monniaux","year":"2001","unstructured":"Monniaux, D.: Backwards abstract interpretation of probabilistic programs. In: Sands, D. (ed.) ESOP 2001. LNCS, vol.\u00a02028, pp. 367\u2013382. Springer, Heidelberg (2001)"},{"issue":"1","key":"6_CR20","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), 179\u2013205 (2005)","journal-title":"Science of Computer Programming"},{"key":"6_CR21","doi-asserted-by":"crossref","unstructured":"Motwani, R., Raghavan, P.: Randomized Algorithms. Cambridge University Press (1995)","DOI":"10.1017\/CBO9780511814075"},{"key":"6_CR22","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan, S., Chakarov, A., Gulwani, S.: Static analysis for probabilistic programs: inferring whole program properties from finitely many paths. In: PLDI, pp. 447\u2013458. ACM (2013)","DOI":"10.1145\/2499370.2462179"},{"key":"6_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/978-3-540-27864-1_7","volume-title":"Static Analysis","author":"S. Sankaranarayanan","year":"2004","unstructured":"Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Constraint-based linear-relations analysis. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol.\u00a03148, pp. 53\u201368. Springer, Heidelberg (2004)"},{"key":"6_CR24","doi-asserted-by":"crossref","unstructured":"Williams, D.: Probability with Martingales. Cambridge University Press (1991)","DOI":"10.1017\/CBO9780511813658"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-10936-7_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T20:23:16Z","timestamp":1558988596000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-10936-7_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319109350","9783319109367"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-10936-7_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}