{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,8]],"date-time":"2025-12-08T07:11:16Z","timestamp":1765177876202,"version":"3.37.3"},"reference-count":51,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2019,1,17]],"date-time":"2019-01-17T00:00:00Z","timestamp":1547683200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["681393"],"award-info":[{"award-number":["681393"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2019,8]]},"DOI":"10.1007\/s10703-019-00331-2","type":"journal-article","created":{"date-parts":[[2019,1,17]],"date-time":"2019-01-17T14:10:37Z","timestamp":1547734237000},"page":"64-109","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Quantitative static analysis of communication protocols using abstract Markov chains"],"prefix":"10.1007","volume":"54","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7248-5914","authenticated-orcid":false,"given":"Abdelraouf","family":"Ouadjaout","sequence":"first","affiliation":[]},{"given":"Antoine","family":"Min\u00e9","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,1,17]]},"reference":[{"issue":"6","key":"331_CR1","doi-asserted-by":"publisher","first-page":"624","DOI":"10.3166\/ejc.16.624-641","volume":"16","author":"A Abate","year":"2010","unstructured":"Abate A, Katoen J-P, Lygeros J, Prandini M (2010) Approximate model checking of stochastic hybrid systems. Eur J Control 16(6):624\u2013641","journal-title":"Eur J Control"},{"key":"331_CR2","unstructured":"Anand S, P\u0103s\u0103reanu, CS, Visser W (2007) JPF-SE: a symbolic execution extension to Java Path Finder. In: TACAS\u201907, volume 4424 of LNCS. Springer, pp 134\u2013138"},{"key":"331_CR3","doi-asserted-by":"crossref","unstructured":"Barthe G, Espitau T, Ferrer Fioriti L, Hsu J (2016) Synthesizing probabilistic invariants via Doob\u2019s decomposition. In: CAV \u201916, volume 9779 of LNCS. Springer, pp 43\u201361","DOI":"10.1007\/978-3-319-41528-4_3"},{"issue":"2","key":"331_CR4","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 (2012) A generalization of p-boxes to affine arithmetic. Computing 94(2):189\u2013201","journal-title":"Computing"},{"key":"331_CR5","doi-asserted-by":"crossref","unstructured":"Bouissou, O, Goubault E, Putot S, Chakarov A, Sankaranarayanan S (2016) Uncertainty propagation using probabilistic affine forms and concentration of measure inequalities. In: TACAS \u201916, volume 9636 of LNCS. Springer, pp 225\u2013243","DOI":"10.1007\/978-3-662-49674-9_13"},{"issue":"1","key":"331_CR6","doi-asserted-by":"publisher","first-page":"59","DOI":"10.2307\/3215235","volume":"31","author":"P Buchholz","year":"1994","unstructured":"Buchholz P (1994) Exact and ordinary lumpability in finite Markov chains. J Appl Probab 31(1):59\u201375","journal-title":"J Appl Probab"},{"key":"331_CR7","doi-asserted-by":"crossref","unstructured":"Chakarov A, Sankaranarayanan S (2013) Probabilistic program analysis with martingales. In: CAV \u201913, volume 8044 of LNCS. Springer, pp 511\u2013526","DOI":"10.1007\/978-3-642-39799-8_34"},{"key":"331_CR8","doi-asserted-by":"crossref","unstructured":"Chakarov A, Sankaranarayanan S (2014) Expectation invariants for probabilistic program loops as fixed points. In: SAS \u201914, volume 8723 of LNCS. Springer, pp 85\u2013100","DOI":"10.1007\/978-3-319-10936-7_6"},{"key":"331_CR9","doi-asserted-by":"crossref","unstructured":"Cousot P, Cousot R (1977) Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL \u201977. ACM, pp 238\u2013252","DOI":"10.1145\/512950.512973"},{"key":"331_CR10","doi-asserted-by":"crossref","unstructured":"Cousot P, Halbwachs N (1978) Automatic discovery of linear restraints among variables of a program. In: POPL \u201978. ACM, pp 84\u201397","DOI":"10.1145\/512760.512770"},{"key":"331_CR11","doi-asserted-by":"crossref","unstructured":"Cousot P, Monerau M (2012) Probabilistic abstract interpretation. In: ESOP \u201912, volume 7211 of LNCS. Springer, pp 169\u2013193","DOI":"10.1007\/978-3-642-28869-2_9"},{"key":"331_CR12","unstructured":"Cousot R (1985) Fondements des m\u00e9thodes de preuve d\u2019invariance et de fatalit\u00e9 de programmes parall\u00e8les. Th\u00e8se d\u2019\u00c9tat \u00e8s sciences math\u00e9matiques, Institut National Polytechnique de Lorraine, Nancy, France"},{"key":"331_CR13","doi-asserted-by":"publisher","DOI":"10.1201\/9781584889878","volume-title":"Performance analysis of queuing and computer networks","author":"GR Dattatreya","year":"2008","unstructured":"Dattatreya GR (2008) Performance analysis of queuing and computer networks. Chapman and Hall\/CRC, Boca Raton"},{"key":"331_CR14","unstructured":"Daws C (2004) Symbolic and parametric model checking of discrete-time Markov chains. In: ICTAC \u201904, volume 3407 of LNCS. Springer, pp 280\u2013294"},{"issue":"4","key":"331_CR15","doi-asserted-by":"publisher","first-page":"1273","DOI":"10.1016\/j.jsc.2003.04.003","volume":"38","author":"JA Loera De","year":"2004","unstructured":"De Loera JA, Hemmecke R, Tauzer J, Yoshida R (2004) Effective lattice point counting in rational convex polytopes. J Symb Comput 38(4):1273\u20131302","journal-title":"J Symb Comput"},{"key":"331_CR16","doi-asserted-by":"crossref","unstructured":"Dehnert C, Junges S, Jansen N, Corzilius F, Volk M, Bruintjes H, Katoen J.-P, \u00c1brah\u00e1m E (2015) PROPhESY: a PRObabilistic ParamEter SYnthesis tool. In: CAV \u201915, volume 9206 of LNCS. Springer, pp 214\u2013231","DOI":"10.1007\/978-3-319-21690-4_13"},{"key":"331_CR17","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511581274","volume-title":"Concentration of measure for the analysis of randomized algorithms","author":"DP Dubhashi","year":"2009","unstructured":"Dubhashi DP, Panconesi A (2009) Concentration of measure for the analysis of randomized algorithms. Cambridge University Press, Cambridge"},{"key":"331_CR18","doi-asserted-by":"crossref","unstructured":"Feret J (2001) Abstract interpretation-based static analysis of mobile ambients. In: SAS \u201901, volume 2126 of LNCS. Springer, pp 412\u2013430","DOI":"10.1007\/3-540-47764-0_24"},{"key":"331_CR19","doi-asserted-by":"crossref","unstructured":"Ferson S, Kreinovick V, Ginzburg L, Sentz F (2003) Constructing probability boxes and Dempster-Shafer structures. Technical report, SAND2002-4015","DOI":"10.2172\/809606"},{"key":"331_CR20","doi-asserted-by":"crossref","unstructured":"Filieri A, P\u0103s\u0103reanu CS, Visser W (2013) Reliability analysis in symbolic pathfinder. In: ICSE \u201913. IEEE Press, pp 622\u2013631","DOI":"10.1109\/ICSE.2013.6606608"},{"key":"331_CR21","doi-asserted-by":"crossref","unstructured":"Filieri A, P\u0103s\u0103reanu CS, Visser W, Geldenhuys J (2014) Statistical symbolic execution with informed sampling. In: FSE \u201914. ACM, pp 437\u2013448","DOI":"10.1145\/2635868.2635899"},{"key":"331_CR22","doi-asserted-by":"crossref","unstructured":"Geldenhuys J, Dwyer MB, Visser W (2012) Probabilistic symbolic execution. In: ISSTA \u201912. ACM, pp 166\u2013176","DOI":"10.1145\/2338965.2336773"},{"key":"331_CR23","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780198572237.001.0001","volume-title":"Probability and random processes","author":"G Grimmett","year":"2001","unstructured":"Grimmett G, Stirzaker D (2001) Probability and random processes. Oxford University Press, Oxford"},{"key":"331_CR24","unstructured":"Gr\u00ef\u00dflinger A (2003) Extending the polyhedron model to inequality systems with non-linear parameters using quantifier elimination. Master thesis, University of Passau"},{"issue":"1","key":"331_CR25","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s10009-010-0146-x","volume":"13","author":"E Hahn","year":"2011","unstructured":"Hahn E, Hermanns H, Zhang L (2011) Probabilistic reachability for parametric Markov models. Int J Softw Tools Technol Transf 13(1):3\u201319","journal-title":"Int J Softw Tools Technol Transf"},{"key":"331_CR26","doi-asserted-by":"crossref","unstructured":"Jeannet B, Min\u00e9 A (2009) Apron: a library of numerical abstract domains for static analysis. In: CAV \u201909, volume 5643 of LNCS. Springer, pp 661\u2013667","DOI":"10.1007\/978-3-642-02658-4_52"},{"key":"331_CR27","volume-title":"Finite Markov chains","author":"JG Kemeney","year":"1976","unstructured":"Kemeney JG, Snell JL (1976) Finite Markov chains. Springer, Berlin"},{"issue":"2","key":"331_CR28","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1016\/0022-0000(85)90012-1","volume":"30","author":"D Kozen","year":"1985","unstructured":"Kozen D (1985) A probabilistic PDL. J Comput Syst Sci 30(2):162\u2013178","journal-title":"J Comput Syst Sci"},{"key":"331_CR29","unstructured":"Kwiatkowska M, Norman G, Parker D (2011) PRISM 4.0: verification of probabilistic real-time systems. In: CAV \u201911, volume 6806 of LNCS. Springer, pp 585\u2013591"},{"key":"331_CR30","doi-asserted-by":"crossref","unstructured":"Le\u00a0Gall T, Jeannet B (2007) Lattice automata: a representation for languages on infinite alphabets, and some applications to verification. In: SAS \u201907, volume 4634 of LNCS. Springer, pp 52\u201368","DOI":"10.1007\/978-3-540-74061-2_4"},{"issue":"1\u20132","key":"331_CR31","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1016\/S0304-3975(00)00104-3","volume":"256","author":"D Lesens","year":"2001","unstructured":"Lesens D, Halbwachs N, Raymond P (2001) Automatic verification of parameterized networks of processes. Theor Comput Sci 256(1\u20132):113\u2013144","journal-title":"Theor Comput Sci"},{"key":"331_CR32","doi-asserted-by":"crossref","unstructured":"Luckow K, P\u0103s\u0103reanu CS, Dwyer MB, Filieri A, Visser W (2014) Exact and approximate probabilistic symbolic execution for nondeterministic programs. In: ASE \u201914. ACM, pp 575\u2013586","DOI":"10.1145\/2642937.2643011"},{"key":"331_CR33","volume-title":"Abstraction, refinement and proof for probabilistic systems. Monographs in Computer Science","author":"A McIver","year":"2004","unstructured":"McIver A, Morgan C (2004) Abstraction, refinement and proof for probabilistic systems. Monographs in Computer Science. Springer, Berlin"},{"issue":"1","key":"331_CR34","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/s10990-006-8609-1","volume":"19","author":"A Min\u00e9","year":"2006","unstructured":"Min\u00e9 A (2006) The octagon abstract domain. Higher Ord Symb Comput (HOSC) 19(1):31\u2013100","journal-title":"Higher Ord Symb Comput (HOSC)"},{"key":"331_CR35","doi-asserted-by":"crossref","unstructured":"Monniaux D (2000) Abstract interpretation of probabilistic semantics. In: SAS \u201900, volume 1824 of LNCS. Springer, pp 322\u2013339","DOI":"10.1007\/978-3-540-45099-3_17"},{"key":"331_CR36","doi-asserted-by":"crossref","unstructured":"Monniaux D (2001) Backwards abstract interpretation of probabilistic programs. In: ESOP \u201901, volume 2028 of LNCS. Springer, pp 367\u2013382","DOI":"10.1007\/3-540-45309-1_24"},{"key":"331_CR37","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 (2005) Abstract interpretation of programs as Markov decision processes. Sci Comput Program 58:179\u2013205","journal-title":"Sci Comput Program"},{"key":"331_CR38","doi-asserted-by":"crossref","unstructured":"Necula G, McPeak S, Rahul S, Weimer W (2002) CIL: intermediate language and tools for analysis and transformation of C programs. In: CC \u201902, pp 213\u2013228","DOI":"10.1007\/3-540-45937-5_16"},{"key":"331_CR39","doi-asserted-by":"crossref","unstructured":"Ouadjaout A, Min\u00e9 A (2017) Quantitative static analysis of communication protocols using abstract Markov chains. In: SAS \u201917, volume 10422 of LNCS. Springer, pp 277\u2013229","DOI":"10.1007\/978-3-319-66706-5_14"},{"issue":"4","key":"331_CR40","doi-asserted-by":"publisher","first-page":"570","DOI":"10.1145\/321356.321364","volume":"13","author":"R Parikh","year":"1966","unstructured":"Parikh R (1966) On context-free languages. J ACM 13(4):570\u2013581","journal-title":"J ACM"},{"key":"331_CR41","doi-asserted-by":"publisher","DOI":"10.1002\/9780470316887","volume-title":"Markov decision processes: discrete stochastic dynamic programming. Wiley Series in Probability and Statistics","author":"ML Puterman","year":"1994","unstructured":"Puterman ML (1994) Markov decision processes: discrete stochastic dynamic programming. Wiley Series in Probability and Statistics. Wiley, Hoboken"},{"key":"331_CR42","volume-title":"Stochastic processes","author":"S Ross","year":"1996","unstructured":"Ross S (1996) Stochastic processes. Wiley, Hoboken"},{"key":"331_CR43","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan S, Chakarov A, Gulwani S (2013) Static analysis for probabilistic programs: inferring whole program properties from finitely many paths. In: PLDI \u201913. ACM, pp 447\u2013458","DOI":"10.1145\/2491956.2462179"},{"key":"331_CR44","doi-asserted-by":"crossref","DOI":"10.1515\/9780691214696","volume-title":"A mathematical theory of evidence","author":"G Shafer","year":"1976","unstructured":"Shafer G (1976) A mathematical theory of evidence. Princeton University Press, Princeton"},{"key":"331_CR45","doi-asserted-by":"crossref","unstructured":"Soudjani SEZ, Abate A (2014) Precise approximations of the probability distribution of a Markov process in time: an application to probabilistic invariance. In: TACAS \u201914, volume 8413 of LNCS. Springer, pp 547\u2013561 (2014)","DOI":"10.1007\/978-3-642-54862-8_45"},{"key":"331_CR46","unstructured":"Suriana P (2016) Fourier\u2013Motzkin with non-linear symbolic constant coefficients. Master thesis, Massachusetts Institute of Technology"},{"issue":"3","key":"331_CR47","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1016\/0743-1066(94)00021-W","volume":"22","author":"P Hentenryck Van","year":"1995","unstructured":"Van Hentenryck P, Cortesi A, Le Charlier B (1995) Type analysis of Prolog using type graphs. J Log Program 22(3):179\u2013209","journal-title":"J Log Program"},{"issue":"2","key":"331_CR48","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1016\/S0167-6423(99)00012-X","volume":"35","author":"A Venet","year":"1999","unstructured":"Venet A (1999) Automatic analysis of pointer aliasing for untyped programs. Sci Comput Program 35(2):223\u2013248","journal-title":"Sci Comput Program"},{"key":"331_CR49","unstructured":"Villemot S (2002) Automates finis et int\u00e9rpretation abstraite: application \u00e0 l\u2019analyse statique de protocoles de communication. Rapport de DEA, \u00c9cole normale sup\u00e9rieure"},{"key":"331_CR50","doi-asserted-by":"crossref","unstructured":"Wang D, Hoffmann J, Reps T (2018) PMAF: an algebraic framework for static analysis of probabilistic programs. In: PLDI \u201918. ACM, pp 513\u2013528","DOI":"10.1145\/3192366.3192408"},{"key":"331_CR51","unstructured":"Wolfram Research, Inc. (2017) Mathematica, Version 11.2, Champaign, IL"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-019-00331-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-019-00331-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-019-00331-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,14]],"date-time":"2024-07-14T05:10:23Z","timestamp":1720933823000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-019-00331-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,17]]},"references-count":51,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2019,8]]}},"alternative-id":["331"],"URL":"https:\/\/doi.org\/10.1007\/s10703-019-00331-2","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2019,1,17]]},"assertion":[{"value":"17 January 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}