{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:49:07Z","timestamp":1740098947797,"version":"3.37.3"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319667058"},{"type":"electronic","value":"9783319667065"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-66706-5_14","type":"book-chapter","created":{"date-parts":[[2017,8,18]],"date-time":"2017-08-18T00:13:26Z","timestamp":1503015206000},"page":"277-298","source":"Crossref","is-referenced-by-count":1,"title":["Quantitative Static Analysis of Communication Protocols Using Abstract Markov Chains"],"prefix":"10.1007","author":[{"given":"Abdelraouf","family":"Ouadjaout","sequence":"first","affiliation":[]},{"given":"Antoine","family":"Min\u00e9","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,8,19]]},"reference":[{"key":"14_CR1","doi-asserted-by":"crossref","unstructured":"Barthe, G., Espitau, T., Ferrer Fioriti, L., Hsu, J.: Synthesizing probabilistic invariants via Doob\u2019s decomposition. In: CAV 2016. LNCS, vol. 9779, pp. 43\u201361. Springer, Cham (2016)","DOI":"10.1007\/978-3-319-41528-4_3"},{"issue":"2","key":"14_CR2","doi-asserted-by":"crossref","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 94(2), 189\u2013201 (2012)","journal-title":"Computing"},{"key":"14_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/978-3-662-49674-9_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"O Bouissou","year":"2016","unstructured":"Bouissou, O., Goubault, E., Putot, S., Chakarov, A., Sankaranarayanan, S.: Uncertainty propagation using probabilistic affine forms and concentration of measure inequalities. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 225\u2013243. Springer, Heidelberg (2016). doi:\n10.1007\/978-3-662-49674-9_13"},{"key":"14_CR4","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. 8044, pp. 511\u2013526. Springer, Heidelberg (2013). doi:\n10.1007\/978-3-642-39799-8_34"},{"key":"14_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/978-3-319-10936-7_6","volume-title":"Static Analysis","author":"A Chakarov","year":"2014","unstructured":"Chakarov, A., Sankaranarayanan, S.: Expectation invariants for probabilistic program loops as fixed points. In: M\u00fcller-Olm, M., Seidl, H. (eds.) SAS 2014. LNCS, vol. 8723, pp. 85\u2013100. Springer, Cham (2014). doi:\n10.1007\/978-3-319-10936-7_6"},{"key":"14_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/978-3-642-11319-2_11","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"L Chen","year":"2010","unstructured":"Chen, L., Min\u00e9, A., Wang, J., Cousot, P.: An abstract domain to discover interval linear equalities. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol. 5944, pp. 112\u2013128. Springer, Heidelberg (2010). doi:\n10.1007\/978-3-642-11319-2_11"},{"key":"14_CR7","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: POPL 1978, pp. 84\u201397. ACM, New York (1978)","DOI":"10.1145\/512760.512770"},{"key":"14_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/978-3-642-28869-2_9","volume-title":"Programming Languages and Systems","author":"P Cousot","year":"2012","unstructured":"Cousot, P., Monerau, M.: Probabilistic abstract interpretation. In: Seidl, H. (ed.) ESOP 2012. LNCS, vol. 7211, pp. 169\u2013193. Springer, Heidelberg (2012). doi:\n10.1007\/978-3-642-28869-2_9"},{"key":"14_CR9","volume-title":"Fondements des M\u00e9thodes de Preuve d\u2019invariance et de fatalit\u00e9 de Programmes Parall\u00e8les","author":"R Cousot","year":"1985","unstructured":"Cousot, R.: 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 (1985)"},{"key":"14_CR10","doi-asserted-by":"crossref","unstructured":"Di Pierro, A., Wiklicky, H.: Concurrent constraint programming: towards probabilistic abstract interpretation. In: PPDP 2000, pp. 127\u2013138. ACM, New York (2000)","DOI":"10.1145\/351268.351284"},{"key":"14_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"412","DOI":"10.1007\/3-540-47764-0_24","volume-title":"Static Analysis","author":"J Feret","year":"2001","unstructured":"Feret, J.: Abstract interpretation-based static analysis of mobile ambients. In: Cousot, P. (ed.) SAS 2001. LNCS, vol. 2126, pp. 412\u2013430. Springer, Heidelberg (2001). doi:\n10.1007\/3-540-47764-0_24"},{"key":"14_CR12","doi-asserted-by":"crossref","unstructured":"Geldenhuys, J., Dwyer, M.B., Visser, W.: Probabilistic symbolic execution. In: ISSTA 2012, pp. 166\u2013176. ACM, New York (2012)","DOI":"10.1145\/2338965.2336773"},{"key":"14_CR13","unstructured":"Gr\u00ef\u00dflinger, A.: Extending the polyhedron model to inequality systems with non-linear parameters using quantifier elimination. Master thesis, University of Passau (2003)"},{"issue":"1","key":"14_CR14","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/s10009-010-0146-x","volume":"13","author":"E Hahn","year":"2011","unstructured":"Hahn, E., Hermanns, H., Zhang, L.: Probabilistic reachability for parametric markov models. Int. J. Softw. Tools Technol. Transf. 13(1), 3\u201319 (2011)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"14_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. 5643, pp. 661\u2013667. Springer, Heidelberg (2009). doi:\n10.1007\/978-3-642-02658-4_52"},{"key":"14_CR16","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. 6806, pp. 585\u2013591. Springer, Heidelberg (2011). doi:\n10.1007\/978-3-642-22110-1_47"},{"key":"14_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/978-3-540-74061-2_4","volume-title":"Static Analysis","author":"T Gall","year":"2007","unstructured":"Gall, T., Jeannet, B.: Lattice automata: a representation for languages on infinite alphabets, and some applications to verification. In: Nielson, H.R., Fil\u00e9, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 52\u201368. Springer, Heidelberg (2007). doi:\n10.1007\/978-3-540-74061-2_4"},{"issue":"1\u20132","key":"14_CR18","doi-asserted-by":"crossref","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.: Automatic verification of parameterized networks of processes. Theor. Comput. Sci. 256(1\u20132), 113\u2013144 (2001)","journal-title":"Theor. Comput. Sci."},{"key":"14_CR19","doi-asserted-by":"crossref","unstructured":"Mardziel, P., Magill, S., Hicks, M., Srivatsa, M.: Dynamic enforcement of knowledge-based security policies. In: CSF 2011, pp. 114\u2013128 (2011)","DOI":"10.1109\/CSF.2011.15"},{"key":"14_CR20","volume-title":"Abstraction, Refinement And Proof For Probabilistic Systems. Monographs in Computer Science","author":"A McIver","year":"2004","unstructured":"McIver, A., Morgan, C.: Abstraction, Refinement And Proof For Probabilistic Systems. Monographs in Computer Science. Springer, New York (2004)"},{"issue":"1","key":"14_CR21","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/s10990-006-8609-1","volume":"19","author":"A Min\u00e9","year":"2006","unstructured":"Min\u00e9, A.: The octagon abstract domain. Higher-Order Symbolic Comput. 19(1), 31\u2013100 (2006)","journal-title":"Higher-Order Symbolic Comput."},{"key":"14_CR22","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: Palsberg, J. (ed.) SAS 2000. LNCS, vol. 1824, pp. 322\u2013339. Springer, Heidelberg (2000). doi:\n10.1007\/978-3-540-45099-3_17"},{"key":"14_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/3-540-45937-5_16","volume-title":"Compiler Construction","author":"GC Necula","year":"2002","unstructured":"Necula, G.C., McPeak, S., Rahul, S.P., Weimer, W.: CIL: intermediate language and tools for analysis and transformation of C programs. In: Horspool, R.N. (ed.) CC 2002. LNCS, vol. 2304, pp. 213\u2013228. Springer, Heidelberg (2002). doi:\n10.1007\/3-540-45937-5_16"},{"issue":"2","key":"14_CR24","doi-asserted-by":"crossref","first-page":"283","DOI":"10.1007\/s10107-003-0433-3","volume":"99","author":"A Neumaier","year":"2004","unstructured":"Neumaier, A., Shcherbina, O.: Safe bounds in linear and mixed-integer linear programming. Math. Program. 99(2), 283\u2013296 (2004)","journal-title":"Math. Program."},{"issue":"4","key":"14_CR25","doi-asserted-by":"crossref","first-page":"570","DOI":"10.1145\/321356.321364","volume":"13","author":"R Parikh","year":"1966","unstructured":"Parikh, R.: On context-free languages. J. ACM 13(4), 570\u2013581 (1966)","journal-title":"J. ACM"},{"key":"14_CR26","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 2013, pp. 447\u2013458. ACM, New York (2013)","DOI":"10.1145\/2491956.2462179"},{"key":"14_CR27","unstructured":"Suriana, P.: Fourier-Motzkin with non-linear symbolic constant coefficients. Master thesis, Massachusetts Institute of Technology (2016)"},{"issue":"3","key":"14_CR28","doi-asserted-by":"crossref","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.: Type analysis of Prolog using type graphs. J. Logic Program. 22(3), 179\u2013209 (1995)","journal-title":"J. Logic Program."},{"issue":"2","key":"14_CR29","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1016\/S0167-6423(99)00012-X","volume":"35","author":"A Venet","year":"1999","unstructured":"Venet, A.: Automatic analysis of pointer aliasing for untyped programs. Sci. Comput. Program. 35(2), 223\u2013248 (1999)","journal-title":"Sci. Comput. Program."},{"key":"14_CR30","unstructured":"Villemot, S.: Automates finis et int\u00e9rpretation abstraite: application \u00e0 l\u2019analyse statique de protocoles de communication. Rapport de DEA, \u00c9cole normale sup\u00e9rieure (2002)"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66706-5_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,8,18]],"date-time":"2017-08-18T00:17:31Z","timestamp":1503015451000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-66706-5_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319667058","9783319667065"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66706-5_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}