{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,6]],"date-time":"2026-02-06T00:40:09Z","timestamp":1770338409507,"version":"3.49.0"},"publisher-location":"Cham","reference-count":43,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783031131844","type":"print"},{"value":"9783031131851","type":"electronic"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,8,7]],"date-time":"2022-08-07T00:00:00Z","timestamp":1659830400000},"content-version":"vor","delay-in-days":218,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We consider the quantitative problem of obtaining lower-bounds on the probability of termination of a given non-deterministic probabilistic program. Specifically, given a non-termination threshold <jats:inline-formula><jats:alternatives><jats:tex-math>$$p \\in [0, 1],$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mi>p<\/mml:mi>\n                    <mml:mo>\u2208<\/mml:mo>\n                    <mml:mo>[<\/mml:mo>\n                    <mml:mn>0<\/mml:mn>\n                    <mml:mo>,<\/mml:mo>\n                    <mml:mn>1<\/mml:mn>\n                    <mml:mo>]<\/mml:mo>\n                    <mml:mo>,<\/mml:mo>\n                  <\/mml:mrow>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula> we aim for certificates proving that the program terminates with probability at least <jats:inline-formula><jats:alternatives><jats:tex-math>$$1-p$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mn>1<\/mml:mn>\n                    <mml:mo>-<\/mml:mo>\n                    <mml:mi>p<\/mml:mi>\n                  <\/mml:mrow>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>. The basic idea of our approach is to find a terminating stochastic invariant, i.e.\u00a0a subset <jats:inline-formula><jats:alternatives><jats:tex-math>$$ SI $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mi>SI<\/mml:mi>\n                  <\/mml:mrow>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula> of program states such that (i)\u00a0the probability of the program ever leaving <jats:inline-formula><jats:alternatives><jats:tex-math>$$ SI $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mi>SI<\/mml:mi>\n                  <\/mml:mrow>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula> is no more than <jats:italic>p<\/jats:italic>, and (ii)\u00a0almost-surely, the program either leaves <jats:inline-formula><jats:alternatives><jats:tex-math>$$ SI $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mi>SI<\/mml:mi>\n                  <\/mml:mrow>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula> or terminates.<\/jats:p><jats:p>While stochastic invariants are already well-known, we provide the first proof that the idea above is not only sound, but also complete for quantitative termination analysis. We then introduce a novel sound and complete characterization of stochastic invariants that enables template-based approaches for easy synthesis of quantitative termination certificates, especially in affine or polynomial forms. Finally, by combining this idea with the existing martingale-based methods that are relatively complete for <jats:italic>qualitative<\/jats:italic> termination analysis, we obtain the first automated, sound, and relatively complete algorithm for <jats:italic>quantitative<\/jats:italic> termination analysis. Notably, our completeness guarantees for quantitative termination analysis are as strong as the best-known methods for the qualitative variant.<\/jats:p><jats:p>Our prototype implementation demonstrates the effectiveness of our approach on various probabilistic programs. We also demonstrate that our algorithm certifies lower bounds on termination probability for probabilistic programs that are beyond the reach of previous methods.<\/jats:p>","DOI":"10.1007\/978-3-031-13185-1_4","type":"book-chapter","created":{"date-parts":[[2022,8,6]],"date-time":"2022-08-06T19:29:09Z","timestamp":1659814149000},"page":"55-78","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":23,"title":["Sound and\u00a0Complete Certificates for\u00a0Quantitative Termination Analysis of\u00a0Probabilistic Programs"],"prefix":"10.1007","author":[{"given":"Krishnendu","family":"Chatterjee","sequence":"first","affiliation":[]},{"given":"Amir Kafshdar","family":"Goharshady","sequence":"additional","affiliation":[]},{"given":"Tobias","family":"Meggendorfer","sequence":"additional","affiliation":[]},{"given":"\u0110or\u0111e","family":"\u017dikeli\u0107","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,8,7]]},"reference":[{"key":"4_CR1","doi-asserted-by":"publisher","unstructured":"Agrawal, S., Chatterjee, K., Novotn\u00fd, P.: Lexicographic ranking supermartingales: an efficient approach to termination of probabilistic programs. In: POPL (2018). https:\/\/doi.org\/10.1145\/3158122","DOI":"10.1145\/3158122"},{"key":"4_CR2","doi-asserted-by":"publisher","unstructured":"Asadi, A., Chatterjee, K., Fu, H., Goharshady, A.K., Mahdavi, M.: Polynomial reachability witnesses via Stellens\u00e4tze. In: PLDI (2021). https:\/\/doi.org\/10.1145\/3453483.3454076","DOI":"10.1145\/3453483.3454076"},{"key":"4_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/978-3-319-41528-4_3","volume-title":"Computer Aided Verification","author":"G Barthe","year":"2016","unstructured":"Barthe, G., Espitau, T., Ferrer Fioriti, L.M., Hsu, J.: Synthesizing probabilistic invariants via Doob\u2019s decomposition. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 43\u201361. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_3"},{"key":"4_CR4","doi-asserted-by":"crossref","unstructured":"Barthe, G., Gaboardi, M., Gr\u00e9goire, B., Hsu, J., Strub, P.Y.: Proving differential privacy via probabilistic couplings. In: LICS (2016). http:\/\/doi.acm.org\/10.1145\/2933575.2934554","DOI":"10.1145\/2933575.2934554"},{"key":"4_CR5","doi-asserted-by":"publisher","unstructured":"Beutner, R., Ong, L.: On probabilistic termination of functional programs with continuous distributions. In: PLDI (2021). https:\/\/doi.org\/10.1145\/3453483.3454111","DOI":"10.1145\/3453483.3454111"},{"key":"4_CR6","unstructured":"Bingham, E., et al.: Pyro: Deep universal probabilistic programming. J. Mach. Learn. Res. (2019). http:\/\/jmlr.org\/papers\/v20\/18-403.html"},{"key":"4_CR7","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). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_34"},{"key":"4_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/978-3-662-49674-9_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Chakarov","year":"2016","unstructured":"Chakarov, A., Voronin, Y.-L., Sankaranarayanan, S.: Deductive proofs of almost sure persistence and recurrence properties. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 260\u2013279. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49674-9_15"},{"key":"4_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-41528-4_1","volume-title":"Computer Aided Verification","author":"K Chatterjee","year":"2016","unstructured":"Chatterjee, K., Fu, H., Goharshady, A.K.: Termination analysis of probabilistic programs through Positivstellensatz\u2019s. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 3\u201322. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_1"},{"key":"4_CR10","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Fu, H., Goharshady, A.K., Goharshady, E.K.: Polynomial invariant generation for non-deterministic recursive programs. In: PLDI (2020). https:\/\/doi.org\/10.1145\/3385412.3385969","DOI":"10.1145\/3385412.3385969"},{"key":"4_CR11","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Fu, H., Novotn\u00fd, P., Hasheminezhad, R.: Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs. TOPLAS 40(2), 7:1\u20137:45 (2018). https:\/\/doi.org\/10.1145\/3174800","DOI":"10.1145\/3174800"},{"key":"4_CR12","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Goharshady, A., Meggendorfer, T., \u017dikeli\u0107, \u0110.: Sound and complete certificates for quantitative termination analysis of probabilistic programs (2022). https:\/\/hal.archives-ouvertes.fr\/hal-03675086","DOI":"10.1007\/978-3-031-13185-1_4"},{"key":"4_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"619","DOI":"10.1007\/978-3-030-90870-6_33","volume-title":"Formal Methods","author":"K Chatterjee","year":"2021","unstructured":"Chatterjee, K., Goharshady, E.K., Novotn\u00fd, P., Z\u00e1rev\u00facky, J., \u017dikeli\u0107, \u0110: On lexicographic proof rules for probabilistic termination. In: Huisman, M., P\u0103s\u0103reanu, C., Zhan, N. (eds.) FM 2021. LNCS, vol. 13047, pp. 619\u2013639. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-90870-6_33"},{"key":"4_CR14","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Novotn\u00fd, P., \u017dikeli\u0107, \u0110.: Stochastic invariants for probabilistic termination. In: POPL (2017). https:\/\/doi.org\/10.1145\/3009837.3009873","DOI":"10.1145\/3009837.3009873"},{"key":"4_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-642-36742-7_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Cimatti","year":"2013","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT solver. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 93\u2013107. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_7"},{"key":"4_CR16","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":"MA Col\u00f3n","year":"2003","unstructured":"Col\u00f3n, M.A., Sankaranarayanan, S., Sipma, H.B.: Linear invariant generation using non-linear constraint solving. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 420\u2013432. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45069-6_39"},{"issue":"124","key":"4_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1515\/crll.1902.124.1","volume":"1902","author":"J Farkas","year":"1902","unstructured":"Farkas, J.: Theorie der einfachen ungleichungen. J. f\u00fcr die reine und angewandte Mathematik 1902(124), 1\u201327 (1902)","journal-title":"J. f\u00fcr die reine und angewandte Mathematik"},{"issue":"1","key":"4_CR18","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1016\/S0019-9958(84)80039-X","volume":"63","author":"YA Feldman","year":"1984","unstructured":"Feldman, Y.A.: A decidable propositional dynamic logic with explicit probabilities. Inf. Control 63(1), 11\u201338 (1984)","journal-title":"Inf. Control"},{"key":"4_CR19","doi-asserted-by":"publisher","unstructured":"Feldman, Y.A., Harel, D.: A probabilistic dynamic logic. In: STOC (1982). https:\/\/doi.org\/10.1145\/800070.802191","DOI":"10.1145\/800070.802191"},{"key":"4_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"282","DOI":"10.1007\/978-3-662-49498-1_12","volume-title":"Programming Languages and Systems","author":"N Foster","year":"2016","unstructured":"Foster, N., Kozen, D., Mamouras, K., Reitblatt, M., Silva, A.: Probabilistic NetKAT. In: Thiemann, P. (ed.) ESOP 2016. LNCS, vol. 9632, pp. 282\u2013309. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49498-1_12"},{"key":"4_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"468","DOI":"10.1007\/978-3-030-11245-5_22","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"H Fu","year":"2019","unstructured":"Fu, H., Chatterjee, K.: Termination of nondeterministic probabilistic programs. In: Enea, C., Piskac, R. (eds.) VMCAI 2019. LNCS, vol. 11388, pp. 468\u2013490. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-11245-5_22"},{"issue":"7553","key":"4_CR22","doi-asserted-by":"publisher","first-page":"452","DOI":"10.1038\/nature14541","volume":"521","author":"Z Ghahramani","year":"2015","unstructured":"Ghahramani, Z.: Probabilistic machine learning and artificial intelligence. Nature 521(7553), 452\u2013459 (2015). https:\/\/doi.org\/10.1038\/nature14541","journal-title":"Nature"},{"key":"4_CR23","unstructured":"Goodman, N.D., et al.: Church: a language for generative models. In: UAI (2008)"},{"key":"4_CR24","doi-asserted-by":"publisher","unstructured":"Hark, M., Kaminski, B.L., Giesl, J., Katoen, J.: Aiming low is harder: induction for lower bounds in probabilistic program verification. In: POPL (2020). https:\/\/doi.org\/10.1145\/3371105","DOI":"10.1145\/3371105"},{"key":"4_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/978-3-030-02768-1_11","volume-title":"Programming Languages and Systems","author":"M Huang","year":"2018","unstructured":"Huang, M., Fu, H., Chatterjee, K.: New approaches for almost-sure termination of probabilistic programs. In: Ryu, S. (ed.) APLAS 2018. LNCS, vol. 11275, pp. 181\u2013201. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-02768-1_11"},{"key":"4_CR26","doi-asserted-by":"publisher","unstructured":"Huang, M., Fu, H., Chatterjee, K., Goharshady, A.K.: Modular verification for almost-sure termination of probabilistic programs. In: OOPSLA (2019). https:\/\/doi.org\/10.1145\/3360555","DOI":"10.1145\/3360555"},{"key":"4_CR27","doi-asserted-by":"publisher","unstructured":"Kaminski, B.L., Katoen, J., Matheja, C., Olmedo, F.: Weakest precondition reasoning for expected runtimes of randomized algorithms. J. ACM 65(5), 30:1\u201330:68 (2018). https:\/\/doi.org\/10.1145\/3208102","DOI":"10.1145\/3208102"},{"key":"4_CR28","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: automated support for proof-based methods. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 390\u2013406. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15769-1_24"},{"issue":"3","key":"4_CR29","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. 22(3), 328\u2013350 (1981). https:\/\/doi.org\/10.1016\/0022-0000(81)90036-2","journal-title":"J. Comput. Syst. Sci."},{"key":"4_CR30","doi-asserted-by":"publisher","unstructured":"K\u0159et\u00ednsk\u00fd, J., Meggendorfer, T.: Of cores: a partial-exploration framework for Markov decision processes. LMCS (2020). https:\/\/doi.org\/10.23638\/LMCS-16(4:3)2020","DOI":"10.23638\/LMCS-16(4:3)2020"},{"key":"4_CR31","doi-asserted-by":"publisher","unstructured":"McIver, A., Morgan, C.: Abstraction, Refinement and Proof for Probabilistic Systems. Monographs in Computer Science. Springer, New York (2005). https:\/\/doi.org\/10.1007\/b138392","DOI":"10.1007\/b138392"},{"key":"4_CR32","doi-asserted-by":"publisher","unstructured":"McIver, A., Morgan, C., Kaminski, B.L., Katoen, J.: A new proof rule for almost-sure termination. In: POPL (2018). https:\/\/doi.org\/10.1145\/3158121","DOI":"10.1145\/3158121"},{"key":"4_CR33","doi-asserted-by":"publisher","DOI":"10.7717\/peerj-cs.103","author":"A Meurer","year":"2017","unstructured":"Meurer, A., et al.: SymPy: symbolic computing in Python. PeerJ Comput. Sci. (2017). https:\/\/doi.org\/10.7717\/peerj-cs.103","journal-title":"PeerJ Comput. Sci."},{"key":"4_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/3-540-47764-0_7","volume-title":"Static Analysis","author":"D Monniaux","year":"2001","unstructured":"Monniaux, D.: An abstract analysis of the probabilistic termination of programs. In: Cousot, P. (ed.) SAS 2001. LNCS, vol. 2126, pp. 111\u2013126. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-47764-0_7"},{"key":"4_CR35","doi-asserted-by":"publisher","unstructured":"Moosbrugger, M., Bartocci, E., Katoen, J., Kov\u00e1cs, L.: Automated termination analysis of polynomial probabilistic programs. In: ESOP (2021). https:\/\/doi.org\/10.1007\/978-3-030-72019-3_18","DOI":"10.1007\/978-3-030-72019-3_18"},{"key":"4_CR36","doi-asserted-by":"publisher","unstructured":"Ngo, V.C., Carbonneaux, Q., Hoffmann, J.: Bounded expectations: resource analysis for probabilistic programs. In: PLDI (2018). https:\/\/doi.org\/10.1145\/3192366.3192394","DOI":"10.1145\/3192366.3192394"},{"key":"4_CR37","doi-asserted-by":"publisher","unstructured":"Olmedo, F., Kaminski, B.L., Katoen, J.P., Matheja, C.: Reasoning about recursive probabilistic programs. In: LICS (2016). https:\/\/doi.org\/10.1145\/2933575.2935317","DOI":"10.1145\/2933575.2935317"},{"issue":"3","key":"4_CR38","doi-asserted-by":"publisher","first-page":"969","DOI":"10.1512\/iumj.1993.42.42045","volume":"42","author":"M Putinar","year":"1993","unstructured":"Putinar, M.: Positive polynomials on compact semi-algebraic sets. Indiana Univ. Math. J. 42(3), 969\u2013984 (1993)","journal-title":"Indiana Univ. Math. J."},{"key":"4_CR39","unstructured":"Roy, D., Mansinghka, V., Goodman, N., Tenenbaum, J.: A stochastic programming perspective on nonparametric Bayes. In: ICML (2008)"},{"key":"4_CR40","doi-asserted-by":"publisher","unstructured":"Takisaka, T., Oyabu, Y., Urabe, N., Hasuo, I.: Ranking and repulsing supermartingales for reachability in randomized programs. ACM Trans. Program. Lang. Syst. 43(2), 5:1\u20135:46 (2021). https:\/\/doi.org\/10.1145\/3450967","DOI":"10.1145\/3450967"},{"issue":"4","key":"4_CR41","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1609\/aimag.v21i4.1534","volume":"21","author":"S Thrun","year":"2000","unstructured":"Thrun, S.: Probabilistic algorithms in robotics. AI Mag. 21(4), 93\u2013109 (2000). https:\/\/doi.org\/10.1609\/aimag.v21i4.1534","journal-title":"AI Mag."},{"key":"4_CR42","doi-asserted-by":"publisher","unstructured":"Wang, J., Sun, Y., Fu, H., Chatterjee, K., Goharshady, A.K.: Quantitative analysis of assertion violations in probabilistic programs. In: PLDI (2021). https:\/\/doi.org\/10.1145\/3453483.3454102","DOI":"10.1145\/3453483.3454102"},{"key":"4_CR43","doi-asserted-by":"publisher","unstructured":"Wang, P., Fu, H., Goharshady, A.K., Chatterjee, K., Qin, X., Shi, W.: Cost analysis of nondeterministic probabilistic programs. In: PLDI (2019). https:\/\/doi.org\/10.1145\/3314221.3314581","DOI":"10.1145\/3314221.3314581"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-13185-1_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,11,3]],"date-time":"2022-11-03T17:12:22Z","timestamp":1667495542000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-13185-1_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031131844","9783031131851"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-13185-1_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"7 August 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Haifa","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Israel","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 August 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 August 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"34","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2022\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-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":"209","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":"40","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":"11","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":"19% - 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.9","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":"9.7","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)"}}]}}