{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,2]],"date-time":"2026-07-02T00:56:03Z","timestamp":1782953763805,"version":"3.54.5"},"publisher-location":"Cham","reference-count":62,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030720155","type":"print"},{"value":"9783030720162","type":"electronic"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,3,20]],"date-time":"2021-03-20T00:00:00Z","timestamp":1616198400000},"content-version":"vor","delay-in-days":78,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We present a novel modular approach to infer upper bounds on the expected runtimes of probabilistic integer programs automatically. To this end, it computes bounds on the runtimes of program parts and on the sizes of their variables in an alternating way. To evaluate its power,\u00a0we implemented our approach in a new version of our open-source tool .<\/jats:p>","DOI":"10.1007\/978-3-030-72016-2_14","type":"book-chapter","created":{"date-parts":[[2021,3,19]],"date-time":"2021-03-19T22:03:37Z","timestamp":1616191417000},"page":"250-269","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":18,"title":["Inferring Expected Runtimes of Probabilistic Integer Programs Using Expected Sizes"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1038-4944","authenticated-orcid":false,"given":"Fabian","family":"Meyer","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5111-3177","authenticated-orcid":false,"given":"Marcel","family":"Hark","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0283-8520","authenticated-orcid":false,"given":"J\u00fcrgen","family":"Giesl","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2021,3,20]]},"reference":[{"key":"14_CR1","doi-asserted-by":"crossref","unstructured":"Agrawal, S., Chatterjee, K., Novotn\u00fd, P.: Lexicographic ranking supermartingales: An efficient approach to termination of probabilistic programs. Proc. ACM Program. Lang. 2(POPL) (2017), https:\/\/doi.org\/10.1145\/3158122","DOI":"10.1145\/3158122"},{"key":"14_CR2","doi-asserted-by":"crossref","unstructured":"Albert, E., Arenas, P., Genaim, S., Puebla, G.: Closed-form upper bounds in static cost analysis. J. Autom. Reasoning 46(2), 161\u2013203 (2011), https:\/\/doi.org\/10.1007\/s10817-010-9174-1","DOI":"10.1007\/s10817-010-9174-1"},{"key":"14_CR3","doi-asserted-by":"crossref","unstructured":"Albert, E., Arenas, P., Genaim, S., Puebla, G., Zanardini, D.: Cost analysis of object-oriented bytecode programs. Theor. Comput. Sci. 413(1), 142\u2013159 (2012), https:\/\/doi.org\/10.1016\/j.tcs.2011.07.009","DOI":"10.1016\/j.tcs.2011.07.009"},{"key":"14_CR4","doi-asserted-by":"crossref","unstructured":"Albert, E., Genaim, S., Masud, A.N.: On the inference of resource usage upper and lower bounds. ACM Trans. Comput. Log. 14(3) (2013), https:\/\/doi.org\/10.1145\/2499937.2499943","DOI":"10.1145\/2499937.2499943"},{"key":"14_CR5","doi-asserted-by":"crossref","unstructured":"Albert, E., Bofill, M., Borralleras, C., Martin-Martin, E., Rubio, A.: Resource analysis driven by (conditional) termination proofs. Theory Pract. Log. Program. 19(5-6), 722\u2013739 (2019), https:\/\/doi.org\/10.1017\/S1471068419000152","DOI":"10.1017\/S1471068419000152"},{"key":"14_CR6","doi-asserted-by":"crossref","unstructured":"Alias, C., Darte, A., Feautrier, P., Gonnord, L.: Multi-dimensional rankings, program termination, and complexity bounds of flowchart programs. In: Proc. SAS\u00a0\u201910. LNCS, vol.\u00a06337, pp. 117\u2013133 (2010), https:\/\/doi.org\/10.1007\/978-3-642-15769-1_8","DOI":"10.1007\/978-3-642-15769-1_8"},{"key":"14_CR7","unstructured":"Ash, R.B., Dol\u00e9ans-Dade, C.A.: Probability and Measure Theory. Harcourt Academic Press, 2nd edn. (2000)"},{"key":"14_CR8","unstructured":"Avanzini, M., Moser, G.: A combination framework for complexity. In: Proc. RTA\u00a013. LIPIcs, vol.\u00a021, pp. 55\u201370 (2013), https:\/\/doi.org\/10.4230\/LIPIcs.RTA.2013.55"},{"key":"14_CR9","doi-asserted-by":"crossref","unstructured":"Avanzini, M., Moser, G., Schaper, M.: TcT: Tyrolean Complexity Tool. In: Proc. TACAS\u00a0\u201916. LNCS, vol.\u00a09636, pp. 407\u2013423 (2016), https:\/\/doi.org\/10.1007\/978-3-662-49674-9_24","DOI":"10.1007\/978-3-662-49674-9_24"},{"key":"14_CR10","doi-asserted-by":"crossref","unstructured":"Avanzini, M., Moser, G., Schaper, M.: A modular cost analysis for probabilistic programs. Proc. ACM Program. Lang. 4(OOPSLA) (2020), https:\/\/doi.org\/10.1145\/3428240","DOI":"10.1145\/3428240"},{"key":"14_CR11","doi-asserted-by":"crossref","unstructured":"Avanzini, M., Dal Lago, U., Yamada, A.: On probabilistic term rewriting. Sci. Comput. Program. 185 (2020), https:\/\/doi.org\/10.1016\/j.scico.2019.102338","DOI":"10.1016\/j.scico.2019.102338"},{"key":"14_CR12","doi-asserted-by":"crossref","unstructured":"Ben-Amram, A.M., Genaim, S.: Ranking functions for linear-constraint loops. J. ACM 61(4) (2014), https:\/\/doi.org\/10.1145\/2629488","DOI":"10.1145\/2629488"},{"key":"14_CR13","doi-asserted-by":"crossref","unstructured":"Ben-Amram, A.M., Genaim, S.: On multiphase-linear ranking functions. In: Proc. CAV\u00a0\u201917. LNCS, vol. 10427, pp. 601\u2013620 (2017), https:\/\/doi.org\/10.1007\/978-3-319-63390-9_32","DOI":"10.1007\/978-3-319-63390-9_32"},{"key":"14_CR14","doi-asserted-by":"crossref","unstructured":"Ben-Amram, A.M., Dom\u00e9nech, J.J., Genaim, S.: Multiphase-linear ranking functions and their relation to recurrent sets. In: Proc. SAS\u00a0\u201919. LNCS, vol. 11822, pp. 459\u2013480 (2019), https:\/\/doi.org\/10.1007\/978-3-030-32304-2_22","DOI":"10.1007\/978-3-030-32304-2_22"},{"key":"14_CR15","doi-asserted-by":"crossref","unstructured":"Bournez, O., Garnier, F.: Proving positive almost-sure termination. In: Proc. RTA\u00a0\u201905. LNCS, vol.\u00a03467, pp. 323\u2013337 (2005), https:\/\/doi.org\/10.1007\/978-3-540-32033-3_24","DOI":"10.1007\/978-3-540-32033-3_24"},{"key":"14_CR16","doi-asserted-by":"crossref","unstructured":"Bournez, O., Garnier, F.: Proving positive almost sure termination under strategies. In: Proc. RTA\u00a0\u201906. LNCS, vol.\u00a04098, pp. 357\u2013371 (2006), https:\/\/doi.org\/10.1007\/11805618_27","DOI":"10.1007\/11805618_27"},{"key":"14_CR17","doi-asserted-by":"crossref","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: Linear ranking with reachability. In: Proc. CAV\u00a0\u201905. LNCS, vol.\u00a03576, pp. 491\u2013504 (2005), https:\/\/doi.org\/10.1007\/11513988_48","DOI":"10.1007\/11513988_48"},{"key":"14_CR18","doi-asserted-by":"crossref","unstructured":"Brockschmidt, M., Emmes, F., Falke, S., Fuhs, C., Giesl, J.: Analyzing runtime and size complexity of integer programs. ACM Trans. Program. Lang. Syst. 38(4) (2016), https:\/\/doi.org\/10.1145\/2866575","DOI":"10.1145\/2866575"},{"key":"14_CR19","doi-asserted-by":"crossref","unstructured":"Burstall, R.M., Darlington, J.: A transformation system for developing recursive programs. J. ACM 24(1), 44\u201367 (1977), https:\/\/doi.org\/10.1145\/321992.321996","DOI":"10.1145\/321992.321996"},{"key":"14_CR20","doi-asserted-by":"crossref","unstructured":"Carbonneaux, Q., Hoffmann, J., Shao, Z.: Compositional certified resource bounds. In: Proc. PLDI\u00a0\u201915. pp. 467\u2013478 (2015), https:\/\/doi.org\/10.1145\/2737924.2737955","DOI":"10.1145\/2737924.2737955"},{"key":"14_CR21","doi-asserted-by":"crossref","unstructured":"Carbonneaux, Q., Hoffmann, J., Reps, T.W., Shao, Z.: Automated resource analysis with Coq proof objects. In: CAV\u00a0\u201917. LNCS, vol. 10427, pp. 64\u201385 (2017), https:\/\/doi.org\/10.1007\/978-3-319-63390-9_4","DOI":"10.1007\/978-3-319-63390-9_4"},{"key":"14_CR22","doi-asserted-by":"crossref","unstructured":"Chakarov, A., Sankaranarayanan, S.: Probabilistic program analysis with martingales. In: Proc. CAV\u00a0\u201913. LNCS, vol.\u00a08044, pp. 511\u2013526 (2013), https:\/\/doi.org\/10.1007\/978-3-642-39799-8_34","DOI":"10.1007\/978-3-642-39799-8_34"},{"key":"14_CR23","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Novotn\u00fd, P., Zikelic, D.: Stochastic invariants for probabilistic termination. In: Proc. POPL\u00a0\u201917. pp. 145\u2013160 (2017), https:\/\/doi.org\/10.1145\/3093333.3009873","DOI":"10.1145\/3093333.3009873"},{"key":"14_CR24","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Fu, H., Novotn\u00fd, P., Hasheminezhad, R.: Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs. ACM Trans. Program. Lang. Syst. 40(2) (2018), https:\/\/doi.org\/10.1145\/3174800","DOI":"10.1145\/3174800"},{"key":"14_CR25","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Fu, H., Novotn\u00fd, P.: Termination analysis of probabilistic programs with martingales. In: Barthe, G., Katoen, J., Silva, A. (eds.) Foundations of Probabilistic Programming, pp. 221\u2014258. Cambridge University Press (2020), https:\/\/doi.org\/10.1017\/9781108770750.008","DOI":"10.1017\/9781108770750.008"},{"key":"14_CR26","doi-asserted-by":"crossref","unstructured":"Ferrer\u00a0Fioriti, L.M., Hermanns, H.: Probabilistic termination: Soundness, completeness, and compositionality. In: Proc. POPL\u00a0\u201915. pp. 489\u2013501 (2015), https:\/\/doi.org\/10.1145\/2676726.2677001","DOI":"10.1145\/2676726.2677001"},{"key":"14_CR27","doi-asserted-by":"crossref","unstructured":"Flores-Montoya, A., H\u00e4hnle, R.: Resource analysis of complex programs with cost equations. In: Proc. APLAS\u00a0\u201914. LNCS, vol.\u00a08858, pp. 275\u2013295 (2014), https:\/\/doi.org\/10.1007\/978-3-319-12736-1_15","DOI":"10.1007\/978-3-319-12736-1_15"},{"key":"14_CR28","doi-asserted-by":"crossref","unstructured":"Flores-Montoya, A.: Upper and lower amortized cost bounds of programs expressed as cost relations. In: Proc. FM\u00a0\u201916. LNCS, vol.\u00a09995, pp. 254\u2013273 (2016), https:\/\/doi.org\/10.1007\/978-3-319-48989-6_16","DOI":"10.1007\/978-3-319-48989-6_16"},{"key":"14_CR29","doi-asserted-by":"crossref","unstructured":"Fu, H., Chatterjee, K.: Termination of nondeterministic probabilistic programs. In: Proc. VMCAI\u00a0\u201919. LNCS, vol. 11388, pp. 468\u2013490 (2019), https:\/\/doi.org\/10.1007\/978-3-030-11245-5_22","DOI":"10.1007\/978-3-030-11245-5_22"},{"key":"14_CR30","doi-asserted-by":"crossref","unstructured":"Giesl, J., Aschermann, C., Brockschmidt, M., Emmes, F., Frohn, F., Fuhs, C., Hensel, J., Otto, C., Pl\u00fccker, M., Schneider-Kamp, P., Str\u00f6der, T., Swiderski, S., Thiemann, R.: Analyzing program termination and complexity automatically with AProVE. J. Autom. Reasoning 58(1), 3\u201331 (2017), https:\/\/doi.org\/10.1007\/s10817-016-9388-y","DOI":"10.1007\/s10817-016-9388-y"},{"key":"14_CR31","doi-asserted-by":"crossref","unstructured":"Giesl, J., Rubio, A., Sternagel, C., Waldmann, J., Yamada, A.: The termination and complexity competition. In: Proc. TACAS\u00a0\u201919. LNCS, vol. 11429, pp. 156\u2013166 (2019), https:\/\/doi.org\/10.1007\/978-3-030-17502-3_10","DOI":"10.1007\/978-3-030-17502-3_10"},{"key":"14_CR32","doi-asserted-by":"crossref","unstructured":"Giesl, J., Giesl, P., Hark, M.: Computing expected runtimes for constant probability programs. In: Proc. CADE\u00a0\u201919. LNAI, vol. 11716, pp. 269\u2013286 (2019), https:\/\/doi.org\/10.1007\/978-3-030-29436-6_16","DOI":"10.1007\/978-3-030-29436-6_16"},{"key":"14_CR33","doi-asserted-by":"crossref","unstructured":"Hark, M., Kaminski, B.L., Giesl, J., Katoen, J.: Aiming low is harder: Induction for lower bounds in probabilistic program verification. Proc. ACM Program. Lang. 4(POPL) (2020), https:\/\/doi.org\/10.1145\/3371105","DOI":"10.1145\/3371105"},{"key":"14_CR34","doi-asserted-by":"crossref","unstructured":"Hoffmann, J., Aehlig, K., Hofmann, M.: Multivariate amortized resource analysis. ACM Trans. Program. Lang. Syst. 34(3) (2012), https:\/\/doi.org\/10.1145\/2362389.2362393","DOI":"10.1145\/2362389.2362393"},{"key":"14_CR35","doi-asserted-by":"crossref","unstructured":"Hoffmann, J., Shao, Z.: Type-based amortized resource analysis with integers and arrays. J. Funct. Program. 25 (2015), https:\/\/doi.org\/10.1017\/S0956796815000192","DOI":"10.1017\/S0956796815000192"},{"key":"14_CR36","doi-asserted-by":"crossref","unstructured":"Hoffmann, J., Das, A., Weng, S.C.: Towards automatic resource bound analysis for OCaml. In: Proc. POPL\u00a0\u201917. pp. 359\u2013373 (2017), https:\/\/doi.org\/10.1145\/3009837.3009842","DOI":"10.1145\/3009837.3009842"},{"key":"14_CR37","doi-asserted-by":"crossref","unstructured":"Huang, M., Fu, H., Chatterjee, K.: New approaches for almost-sure termination of probabilistic programs. In: Proc. APLAS\u00a0\u201918. LNCS, vol. 11275, pp. 181\u2013201 (2018), https:\/\/doi.org\/10.1007\/978-3-030-02768-1_11","DOI":"10.1007\/978-3-030-02768-1_11"},{"key":"14_CR38","doi-asserted-by":"crossref","unstructured":"Huang, M., Fu, H., Chatterjee, K., Goharshady, A.K.: Modular verification for almost-sure termination of probabilistic programs. Proc. ACM Program. Lang. 3(OOPSLA) (2019), https:\/\/doi.org\/10.1145\/3360555","DOI":"10.1145\/3360555"},{"key":"14_CR39","doi-asserted-by":"crossref","unstructured":"Jeannet, B., Min\u00e9, A.: Apron: A library of numerical abstract domains for static analysis. In: Proc. CAV\u00a0\u201909. pp. 661\u2013667 (2009), https:\/\/doi.org\/10.1007\/978-3-642-02658-4_52","DOI":"10.1007\/978-3-642-02658-4_52"},{"key":"14_CR40","doi-asserted-by":"crossref","unstructured":"Kallenberg, O.: Foundations of Modern Probability. Springer, New York (2002), https:\/\/doi.org\/10.1007\/978-1-4757-4015-8","DOI":"10.1007\/978-1-4757-4015-8"},{"key":"14_CR41","doi-asserted-by":"crossref","unstructured":"Kaminski, B.L., Katoen, J., Matheja, C., Olmedo, F.: Weakest precondition reasoning for expected runtimes of randomized algorithms. J. ACM 65 (2018), https:\/\/doi.org\/10.1145\/3208102","DOI":"10.1145\/3208102"},{"key":"14_CR42","doi-asserted-by":"crossref","unstructured":"Kaminski, B.L., Katoen, J., Matheja, C.: Expected runtime analyis by program verification. In: Barthe, G., Katoen, J., Silva, A. (eds.) Foundations of Probabilistic Programming, pp. 185\u2014220. Cambridge University Press (2020), https:\/\/doi.org\/10.1017\/9781108770750.007","DOI":"10.1017\/9781108770750.007"},{"key":"14_CR43","unstructured":"KoAT: Web interface, binary, Docker image, and examples available at the web site https:\/\/aprove-developers.github.io\/ExpectedUpperBounds\/. The source code is available at https:\/\/github.com\/aprove-developers\/KoAT2-Releases\/tree\/probabilistic."},{"key":"14_CR44","doi-asserted-by":"crossref","unstructured":"Kozen, D.: Semantics of probabilistic programs. J. Comput. Syst. Sci. 22(3), 328\u2013350 (1981), https:\/\/doi.org\/10.1016\/0022-0000(81)90036-2","DOI":"10.1016\/0022-0000(81)90036-2"},{"key":"14_CR45","doi-asserted-by":"crossref","unstructured":"McIver, A., Morgan, C.: Abstraction, Refinement and Proof for Probabilistic Systems. Springer (2005), https:\/\/doi.org\/10.1007\/b138392","DOI":"10.1007\/b138392"},{"key":"14_CR46","doi-asserted-by":"crossref","unstructured":"McIver, A., Morgan, C., Kaminski, B.L., Katoen, J.: A new proof rule for almost-sure termination. Proc. ACM Program. Lang. 2(POPL) (2018), https:\/\/doi.org\/10.1145\/3158121","DOI":"10.1145\/3158121"},{"key":"14_CR47","unstructured":"Meyer, F., Hark, M., Giesl, J.: Inferring expected runtimes of probabilistic integer programs using expected sizes. CoRR abs\/2010.06367 (2020), https:\/\/arxiv.org\/abs\/2010.06367"},{"key":"14_CR48","doi-asserted-by":"crossref","unstructured":"Moosbrugger, M., Bartocci, E., Katoen, J., Kov\u00e1cs, L.: Automated termination analysis of polynomial probabilistic programs. In: Proc. ESOP \u201921. LNCS (2021), to appear.","DOI":"10.26226\/morressier.604907f41a80aac83ca25d19"},{"key":"14_CR49","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Proc. TACAS\u00a0\u201908. LNCS, vol.\u00a04963, pp. 337\u2013340 (2008), https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"14_CR50","unstructured":"Ngo, V.C., Carbonneaux, Q., Hoffmann, J.: Bounded expectations: Resource analysis for probabilistic programs. In: Proc. PLDI\u00a0\u201918. pp. 496\u2013512 (2018), https:\/\/doi.org\/10.1145\/3192366.3192394, tool artifact and benchmarks available from https:\/\/channgo2203.github.io\/zips\/tool_benchmark.zip"},{"key":"14_CR51","doi-asserted-by":"crossref","unstructured":"Noschinski, L., Emmes, F., Giesl, J.: Analyzing innermost runtime complexity of term rewriting by dependency pairs. J. Autom. Reasoning 51(1), 27\u201356 (2013), https:\/\/doi.org\/10.1007\/s10817-013-9277-6","DOI":"10.1007\/s10817-013-9277-6"},{"key":"14_CR52","doi-asserted-by":"crossref","unstructured":"Olmedo, F., Kaminski, B.L., Katoen, J., Matheja, C.: Reasoning about recursive probabilistic programs. In: Proc. LICS\u00a0\u201916. pp. 672\u2013681 (2016), https:\/\/doi.org\/10.1145\/2933575.2935317","DOI":"10.1145\/2933575.2935317"},{"key":"14_CR53","doi-asserted-by":"crossref","unstructured":"Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: Proc. VMCAI\u00a0\u201904. LNCS, vol.\u00a02937, pp. 239\u2013251 (2004), https:\/\/doi.org\/10.1007\/978-3-540-24622-0_20","DOI":"10.1007\/978-3-540-24622-0_20"},{"key":"14_CR54","unstructured":"Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. John Wiley & Sons (2005)"},{"key":"14_CR55","unstructured":"RaML (Resource Aware ML), https:\/\/www.raml.co\/interface\/"},{"key":"14_CR56","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Constraint-based linear-relations analysis. In: Proc. SAS\u00a0\u201904. LNCS, vol.\u00a03148, pp. 53\u201368 (2004), https:\/\/doi.org\/10.1007\/978-3-540-27864-1_7","DOI":"10.1007\/978-3-540-27864-1_7"},{"key":"14_CR57","doi-asserted-by":"crossref","unstructured":"Sinn, M., Zuleger, F., Veith, H.: Complexity and resource bound analysis of imperative programs using difference constraints. J. Autom. Reasoning 59(1), 3\u201345 (2017), https:\/\/doi.org\/10.1007\/s10817-016-9402-4","DOI":"10.1007\/s10817-016-9402-4"},{"key":"14_CR58","doi-asserted-by":"crossref","unstructured":"Srikanth, A., Sahin, B., Harris, W.R.: Complexity verification using guided theorem enumeration. In: Proc. POPL\u00a0\u201917. pp. 639\u2013652 (2017), https:\/\/doi.org\/10.1145\/3009837.3009864","DOI":"10.1145\/3009837.3009864"},{"key":"14_CR59","unstructured":"TPDB (Termination Problems Data Base), http:\/\/termination-portal.org\/wiki\/TPDB"},{"key":"14_CR60","doi-asserted-by":"crossref","unstructured":"Vardi, M.Y.: Automatic verification of probabilistic concurrent finite-state programs. In: Proc. FOCS\u00a0\u201985. pp. 327\u2013338 (1985), https:\/\/doi.org\/10.1109\/SFCS.1985.12","DOI":"10.1109\/SFCS.1985.12"},{"key":"14_CR61","doi-asserted-by":"crossref","unstructured":"Wang, D., Kahn, D.M., Hoffmann, J.: Raising expectations: automating expected cost analysis with types. Proc. ACM Program. Lang. 4(ICFP) (2020), https:\/\/doi.org\/10.1145\/3408992","DOI":"10.1145\/3408992"},{"key":"14_CR62","doi-asserted-by":"crossref","unstructured":"Wang, P., Fu, H., Goharshady, A.K., Chatterjee, K., Qin, X., Shi, W.: Cost analysis of nondeterministic probabilistic programs. In: Proc. PLDI\u00a0\u201919. pp. 204\u2013220 (2019), https:\/\/doi.org\/10.1145\/3314221.3314581","DOI":"10.1145\/3314221.3314581"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-72016-2_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,29]],"date-time":"2021-04-29T20:35:44Z","timestamp":1619728544000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-72016-2_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030720155","9783030720162"],"references-count":62,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-72016-2_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"20 March 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 March 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 April 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2021\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"141","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"41","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"21","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"29% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"12","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference changed to an online format due to the COVID-19 pandemic","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}