{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T19:50:47Z","timestamp":1776887447695,"version":"3.51.2"},"publisher-location":"Cham","reference-count":110,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031986789","type":"print"},{"value":"9783031986796","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,7,22]],"date-time":"2025-07-22T00:00:00Z","timestamp":1753142400000},"content-version":"vor","delay-in-days":202,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>We introduce a general methodology for quantitative model checking and control synthesis with supermartingale certificates. We show that every specification that is invariant to time shifts admits a stochastic invariant that bounds its probability from below; for systems with general state space, the stochastic invariant bounds this probability as closely as desired; for systems with finite state space, it quantifies it exactly. Our result enables the extension of every certificate for the almost-sure satisfaction of shift-invariant specifications to its quantitative counterpart, ensuring completeness up to an approximation in the general case and exactness in the finite-state case. This generalises and unifies existing supermartingale certificates for quantitative verification and control\u00a0under reachability, safety, reach-avoidance, and stability specifications, as well as asymptotic bounds on accrued costs and rewards. Furthermore, our result provides the first supermartingale certificate for computing upper and lower bounds on the probability of satisfying <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$\\omega $$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>\u03c9<\/mml:mi>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>-regular and linear temporal logic specifications. We present an algorithm for quantitative <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$\\omega $$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>\u03c9<\/mml:mi>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>-regular verification and control synthesis based on our method and demonstrate its practical efficacy on several infinite-state examples.<\/jats:p>","DOI":"10.1007\/978-3-031-98679-6_1","type":"book-chapter","created":{"date-parts":[[2025,7,21]],"date-time":"2025-07-21T09:19:30Z","timestamp":1753089570000},"page":"3-28","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Quantitative Supermartingale Certificates"],"prefix":"10.1007","author":[{"given":"Alessandro","family":"Abate","sequence":"first","affiliation":[]},{"given":"Mirco","family":"Giacobbe","sequence":"additional","affiliation":[]},{"given":"Diptarko","family":"Roy","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,7,22]]},"reference":[{"key":"1_CR1","unstructured":"Abate, A., Edwards, A., Giacobbe, M., Punchihewa, H., Roy, D.: Quantitative verification with neural networks. In: CONCUR. LIPIcs, vol.\u00a0279, pp. 22:1\u201322:18. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2023)"},{"key":"1_CR2","doi-asserted-by":"crossref","unstructured":"Abate, A., Giacobbe, M., Micheletti, C., Schnitzer, Y.: Branching bisimulation learning. In: CAV (2025)","DOI":"10.1007\/978-3-031-98685-7_8"},{"key":"1_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-81688-9_1","volume-title":"Computer Aided Verification","author":"A Abate","year":"2021","unstructured":"Abate, A., Giacobbe, M., Roy, D.: Learning probabilistic termination proofs. In: Silva, A., Leino, K. (eds.) CAV 2021. LNCS, vol. 12760, pp. 3\u201326. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_1"},{"key":"1_CR4","doi-asserted-by":"publisher","unstructured":"Abate, A., Giacobbe, M., Roy, D.: Stochastic omega-regular verification and control with supermartingales. In: CAV (3). Lecture Notes in Computer Science, vol. 14683, pp. 395\u2013419. Springer, Heidelberg (2024). https:\/\/doi.org\/10.1007\/978-3-031-65633-0_18","DOI":"10.1007\/978-3-031-65633-0_18"},{"key":"1_CR5","doi-asserted-by":"publisher","unstructured":"Abate, A., Giacobbe, M., Roy, D., Schnitzer, Y.: Model checking and strategy synthesis with abstractions and certificates. In: Principles of Verification: Cycling the Probabilistic Landscape: Essays Dedicated to Joost-Pieter Katoen on the Occasion of His 60th Birthday, Part II. Lecture Notes in Computer Science, vol. 12261, pp. 360\u2013391. Springer, Heidelberg (2024). https:\/\/doi.org\/10.1007\/978-3-031-75775-4_16","DOI":"10.1007\/978-3-031-75775-4_16"},{"key":"1_CR6","doi-asserted-by":"publisher","unstructured":"Abate, A., Giacobbe, M., Schnitzer, Y.: Bisimulation learning. In: CAV (3). Lecture Notes in Computer Science, vol. 14683, pp. 161\u2013183. Springer, Heidelberg (2024). https:\/\/doi.org\/10.1007\/978-3-031-65633-0_8","DOI":"10.1007\/978-3-031-65633-0_8"},{"key":"1_CR7","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), 34:1\u201334:32 (2018)","DOI":"10.1145\/3158122"},{"key":"1_CR8","doi-asserted-by":"publisher","first-page":"2529","DOI":"10.1109\/LCSYS.2024.3498897","volume":"8","author":"D Ajeleye","year":"2024","unstructured":"Ajeleye, D., Zamani, M.: Co-b\u00fcchi control barrier certificates for stochastic control systems. IEEE Control. Syst. Lett. 8, 2529\u20132534 (2024)","journal-title":"IEEE Control. Syst. Lett."},{"issue":"3","key":"1_CR9","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/BF01782772","volume":"2","author":"B Alpern","year":"1987","unstructured":"Alpern, B., Schneider, F.B.: Recognizing safety and liveness. Distrib. Comput. 2(3), 117\u2013126 (1987)","journal-title":"Distrib. Comput."},{"key":"1_CR10","doi-asserted-by":"publisher","unstructured":"Ansaripour, M., Chatterjee, K., Henzinger, T.A., Lechner, M., Zikelic, D.: Learning provably stabilizing neural controllers for discrete-time stochastic systems. In: ATVA (1). Lecture Notes in Computer Science, vol. 14215, pp. 357\u2013379. Springer, Heidelberg (2023). https:\/\/doi.org\/10.1007\/978-3-031-45329-8_17","DOI":"10.1007\/978-3-031-45329-8_17"},{"key":"1_CR11","doi-asserted-by":"crossref","unstructured":"Asadi, A., Chatterjee, K., Fu, H., Goharshady, A.K., Mahdavi, M.: Polynomial reachability witnesses via stellens\u00e4tze. In: PLDI, pp. 772\u2013787. ACM (2021)","DOI":"10.1145\/3453483.3454076"},{"key":"1_CR12","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"1_CR13","doi-asserted-by":"publisher","unstructured":"Batz, K., Chen, M., Junges, S., Kaminski, B.L., Katoen, J., Matheja, C.: Probabilistic program verification via inductive synthesis of inductive invariants. In: TACAS (2). Lecture Notes in Computer Science, vol. 13994, pp. 410\u2013429. Springer, Heidelberg (2023). https:\/\/doi.org\/10.1007\/978-3-031-30820-8_25","DOI":"10.1007\/978-3-031-30820-8_25"},{"key":"1_CR14","doi-asserted-by":"publisher","unstructured":"Bj\u00f8rner, N.S., Nachmanson, L.: Arithmetic solving in Z3. In: CAV (1). Lecture Notes in Computer Science, vol. 14681, pp. 26\u201341. Springer, Heidelberg (2024). https:\/\/doi.org\/10.1007\/978-3-031-65627-9_2","DOI":"10.1007\/978-3-031-65627-9_2"},{"key":"1_CR15","doi-asserted-by":"crossref","unstructured":"Blute, R., Desharnais, J., Edalat, A., Panangaden, P.: Bisimulation for labelled markov processes. In: LICS, pp. 149\u2013158. IEEE Computer Society (1997)","DOI":"10.1109\/LICS.1997.614943"},{"key":"1_CR16","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":"1_CR17","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"},{"issue":"1\u20133","key":"1_CR18","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1016\/j.tcs.2007.07.047","volume":"388","author":"K Chatterjee","year":"2007","unstructured":"Chatterjee, K.: Concurrent games with tail objectives. Theor. Comput. Sci. 388(1\u20133), 181\u2013198 (2007)","journal-title":"Theor. Comput. Sci."},{"key":"1_CR19","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Fu, H., Goharshady, A.K.: Termination analysis of probabilistic programs through Positivstellensatz. In: CAV (1). Lecture Notes in Computer Science, vol.\u00a09779, pp. 3\u201322. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_1","DOI":"10.1007\/978-3-319-41528-4_1"},{"key":"1_CR20","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), 7:1\u20137:45 (2018)","DOI":"10.1145\/3174800"},{"key":"1_CR21","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Goharshady, A.K., Goharshady, E.K., Karrabi, M., Zikelic, D.: Sound and complete witnesses for template-based verification of LTL properties on polynomial programs. In: FM (1). Lecture Notes in Computer Science, vol. 14933, pp. 600\u2013619. Springer, Heidelberg (2024). https:\/\/doi.org\/10.1007\/978-3-031-71162-6_31","DOI":"10.1007\/978-3-031-71162-6_31"},{"key":"1_CR22","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Goharshady, A.K., Meggendorfer, T., \u017dikeli\u0107, \u0110.: Sound and complete certificates for quantitative termination analysis of probabilistic programs. In: CAV (1). Lecture Notes in Computer Science, vol. 13371, pp. 55\u201378. Springer, Heidelberg (2022). https:\/\/doi.org\/10.1007\/978-3-031-13185-1_4","DOI":"10.1007\/978-3-031-13185-1_4"},{"issue":"OOPSLA1","key":"1_CR23","doi-asserted-by":"publisher","first-page":"362","DOI":"10.1145\/3649824","volume":"8","author":"K Chatterjee","year":"2024","unstructured":"Chatterjee, K., Goharshady, A.K., Meggendorfer, T., \u017dikeli\u0107, \u0110: Quantitative bounds on resource usage of probabilistic programs. Proc. ACM Program. Lang. 8(OOPSLA1), 362\u2013391 (2024)","journal-title":"Proc. ACM Program. Lang."},{"key":"1_CR24","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Goharshady, E.K., Karrabi, M., Motwani, H.J., Seeliger, M., Zikelic, D.: Quantified linear and polynomial arithmetic satisfiability via template-based skolemization. In: AAAI, pp. 7326\u20137336. AAAI Press (2025)","DOI":"10.1609\/aaai.v39i11.33213"},{"key":"1_CR25","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Goharshady, E.K., Novotn\u00fd, P., Zikelic, D.: Equivalence and similarity refutation for probabilistic programs. Proc. ACM Program. Lang. 8(PLDI), 2098\u20132122 (2024)","DOI":"10.1145\/3656462"},{"key":"1_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1007\/978-3-642-03816-7_4","volume-title":"Mathematical Foundations of Computer Science 2009","author":"K Chatterjee","year":"2009","unstructured":"Chatterjee, K., Henzinger, T.A., Horn, F.: Stochastic games with finitary objectives. In: Kr\u00e1lovi\u010d, R., Niwi\u0144ski, D. (eds.) MFCS 2009. LNCS, vol. 5734, pp. 34\u201354. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03816-7_4"},{"key":"1_CR27","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Henzinger, T.A., Lechner, M., Zikelic, D.: A learner-verifier framework for neural network controllers and certificates of stochastic systems. In: TACAS (1). Lecture Notes in Computer Science, vol. 13993, pp. 3\u201325. Springer, Heidelberg (2023). https:\/\/doi.org\/10.1007\/978-3-031-30823-9_1","DOI":"10.1007\/978-3-031-30823-9_1"},{"key":"1_CR28","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Novotn\u00fd, P., \u017dikeli\u0107, \u0110.: Stochastic invariants for probabilistic termination. In: POPL, pp. 145\u2013160. ACM (2017)","DOI":"10.1145\/3009837.3009873"},{"key":"1_CR29","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Quatmann, T., Sch\u00e4ffeler, M., Weininger, M., Winkler, T., Zilken, D.: Fixed point certificates for reachability and expected rewards in mdps. In: TACAS. Lecture Notes in Computer Science (2025)","DOI":"10.1007\/978-3-031-90653-4_7"},{"key":"1_CR30","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"},{"key":"1_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/3-540-45319-9_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"MA Col\u00f3on","year":"2001","unstructured":"Col\u00f3on, M.A., Sipma, H.B.: Synthesis of linear ranking functions. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 67\u201381. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45319-9_6"},{"key":"1_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"442","DOI":"10.1007\/3-540-45657-0_36","volume-title":"Computer Aided Verification","author":"MA Col\u00f3n","year":"2002","unstructured":"Col\u00f3n, M.A., Sipma, H.B.: Practical methods for proving program termination. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 442\u2013454. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45657-0_36"},{"key":"1_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"592","DOI":"10.1007\/978-3-319-63390-9_31","volume-title":"Computer Aided Verification","author":"C Dehnert","year":"2017","unstructured":"Dehnert, C., Junges, S., Katoen, J.-P., Volk, M.: A storm is coming: a modern probabilistic model checker. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 592\u2013600. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63390-9_31"},{"key":"1_CR34","doi-asserted-by":"crossref","unstructured":"Desharnais, J., Laviolette, F., Tracol, M.: Approximate analysis of probabilistic processes: logic, simulation and games. In: QEST, pp. 264\u2013273. IEEE Computer Society (2008)","DOI":"10.1109\/QEST.2008.42"},{"key":"1_CR35","doi-asserted-by":"publisher","unstructured":"Dimitrova, R., Fioriti, L.M.F., Hermanns, H., Majumdar, R.: Probabilistic ctl$$ ^{\\text{*}}$$: the deductive way. In: TACAS. Lecture Notes in Computer Science, vol.\u00a09636, pp. 280\u2013296. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49674-9_16","DOI":"10.1007\/978-3-662-49674-9_16"},{"key":"1_CR36","doi-asserted-by":"crossref","unstructured":"Dimitrova, R., Majumdar, R.: Deductive control synthesis for alternating-time logics. In: EMSOFT, pp. 14:1\u201314:10. ACM (2014)","DOI":"10.1145\/2656045.2656054"},{"key":"1_CR37","doi-asserted-by":"crossref","unstructured":"Douc, R., Moulines, E., Priouret, P., Soulier, P.: Markov Chains. Springer Series in Operations Research and Financial Engineering. Springer, Heidelberg (2018)","DOI":"10.1007\/978-3-319-97704-1"},{"key":"1_CR38","doi-asserted-by":"publisher","unstructured":"Duret-Lutz, A., et al.: From spot 2.0 to spot 2.10: what\u2019s new? In: CAV (2). Lecture Notes in Computer Science, vol. 13372, pp. 174\u2013187. Springer, Heidelberg (2022). https:\/\/doi.org\/10.1007\/978-3-031-13188-2_9","DOI":"10.1007\/978-3-031-13188-2_9"},{"key":"1_CR39","series-title":"Cambridge Series in Statistical and Probabilistic Mathematics","doi-asserted-by":"publisher","DOI":"10.1017\/9781108591034","volume-title":"Probability: Theory and Examples","author":"R Durrett","year":"2019","unstructured":"Durrett, R.: Probability: Theory and Examples. Cambridge Series in Statistical and Probabilistic Mathematics, 5th edn. Cambridge University Press, Cambridge (2019)","edition":"5"},{"issue":"1\u20133","key":"1_CR40","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/j.scico.2007.01.015","volume":"69","author":"MD Ernst","year":"2007","unstructured":"Ernst, M.D., Perkins, J.H., Guo, P.J., McCamant, S., Pacheco, C., Tschantz, M.S., Xiao, C.: The daikon system for dynamic detection of likely invariants. Sci. Comput. Program. 69(1\u20133), 35\u201345 (2007)","journal-title":"Sci. Comput. Program."},{"key":"1_CR41","volume-title":"An Introduction to Probability Theory and its Applications","author":"W Feller","year":"1968","unstructured":"Feller, W.: An Introduction to Probability Theory and its Applications, vol. 1. Wiley, Hoboken (1968)"},{"key":"1_CR42","doi-asserted-by":"crossref","unstructured":"Feng, S., Chen, M., Su, H., Kaminski, B.L., Katoen, J., Zhan, N.: Lower bounds for possibly divergent probabilistic programs. CoRR arxiv:2302.06082 (2023)","DOI":"10.1145\/3586051"},{"key":"1_CR43","doi-asserted-by":"crossref","unstructured":"Fioriti, L.M.F., Hermanns, H.: Probabilistic termination: soundness, completeness, and compositionality. In: POPL, pp. 489\u2013501. ACM (2015)","DOI":"10.1145\/2676726.2677001"},{"key":"1_CR44","doi-asserted-by":"publisher","unstructured":"Floyd, R.W.: Assigning meanings to programs. In: Program Verification: Fundamental Issues in Computer Science, pp. 65\u201381. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/978-94-011-1793-7_4","DOI":"10.1007\/978-94-011-1793-7_4"},{"key":"1_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/978-3-642-21455-4_3","volume-title":"Formal Methods for Eternal Networked Software Systems","author":"V Forejt","year":"2011","unstructured":"Forejt, V., Kwiatkowska, M., Norman, G., Parker, D.: Automated verification techniques for probabilistic systems. In: Bernardo, M., Issarny, V. (eds.) SFM 2011. LNCS, vol. 6659, pp. 53\u2013113. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-21455-4_3"},{"key":"1_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/978-3-642-19835-9_11","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"V Forejt","year":"2011","unstructured":"Forejt, V., Kwiatkowska, M., Norman, G., Parker, D., Qu, H.: Quantitative multi-objective verification for probabilistic systems. In: Abdulla, P.A., Leino, K. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 112\u2013127. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-19835-9_11"},{"key":"1_CR47","doi-asserted-by":"publisher","unstructured":"Gehr, T., Misailovic, S., Vechev, M.T.: PSI: exact symbolic inference for probabilistic programs. In: CAV (1). Lecture Notes in Computer Science, vol.\u00a09779, pp. 62\u201383. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_4","DOI":"10.1007\/978-3-319-41528-4_4"},{"key":"1_CR48","unstructured":"Giacobbe, M., Kroening, D., Pal, A., Tautschnig, M.: Neural model checking. In: NeurIPS (2024)"},{"key":"1_CR49","doi-asserted-by":"crossref","unstructured":"Giacobbe, M., Kroening, D., Parsert, J.: Neural termination analysis. In: ESEC\/SIGSOFT FSE, pp. 633\u2013645. ACM (2022)","DOI":"10.1145\/3540250.3549120"},{"key":"1_CR50","doi-asserted-by":"crossref","unstructured":"Gr\u00e4del, E., Thomas, W., Wilke, T. (eds.): Automata, Logics, and Infinite Games: A Guide to Current Research [outcome of a Dagstuhl seminar, February 2001], Lecture Notes in Computer Science, vol.\u00a02500. Springer, Heidelberg (2002)","DOI":"10.1007\/3-540-36387-4"},{"key":"1_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1007\/978-3-319-06410-9_22","volume-title":"FM 2014: Formal Methods","author":"EM Hahn","year":"2014","unstructured":"Hahn, E.M., Li, Y., Schewe, S., Turrini, A., Zhang, L.: iscasMc: a web-based probabilistic model checker. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 312\u2013317. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-06410-9_22"},{"key":"1_CR52","series-title":"Dover Books on Mathematics","volume-title":"Theory and Application of Liapunov\u2019s Direct Method","author":"W Hahn","year":"2019","unstructured":"Hahn, W.: Theory and Application of Liapunov\u2019s Direct Method. Dover Books on Mathematics, Dover Publications, New York (2019)"},{"key":"1_CR53","doi-asserted-by":"crossref","unstructured":"Handelman, D.: Representing polynomials by positive linear functions on compact convex polyhedra. Pacific J. Math. 132 (1988)","DOI":"10.2140\/pjm.1988.132.35"},{"key":"1_CR54","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), 37:1\u201337:28 (2020)","DOI":"10.1145\/3371105"},{"key":"1_CR55","doi-asserted-by":"crossref","unstructured":"Hasuo, I., Shimizu, S., C\u00eerstea, C.: Lattice-theoretic progress measures and coalgebraic model checking. In: POPL, pp. 718\u2013732. ACM (2016)","DOI":"10.1145\/2837614.2837673"},{"issue":"4","key":"1_CR56","doi-asserted-by":"publisher","first-page":"589","DOI":"10.1007\/s10009-021-00633-z","volume":"24","author":"C Hensel","year":"2022","unstructured":"Hensel, C., Junges, S., Katoen, J., Quatmann, T., Volk, M.: The probabilistic model checker storm. Int. J. Softw. Tools Technol. Transf. 24(4), 589\u2013610 (2022)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"1_CR57","doi-asserted-by":"crossref","unstructured":"Huang, C., Chen, X., Lin, W., Yang, Z., Li, X.: Probabilistic safety verification of stochastic hybrid systems using barrier certificates. ACM Trans. Embed. Comput. Syst. 16(5s), 186:1\u2013186:19 (2017)","DOI":"10.1145\/3126508"},{"key":"1_CR58","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), 129:1\u2013129:29 (2019)","DOI":"10.1145\/3360555"},{"key":"1_CR59","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/978-3-030-01090-4_11","volume-title":"Automated Technology for Verification and Analysis","author":"P Jagtap","year":"2018","unstructured":"Jagtap, P., Soudjani, S., Zamani, M.: Temporal logic verification of stochastic systems using barrier certificates. In: Lahiri, S.K., Wang, C. (eds.) ATVA 2018. LNCS, vol. 11138, pp. 177\u2013193. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-01090-4_11"},{"issue":"7","key":"1_CR60","doi-asserted-by":"publisher","first-page":"3097","DOI":"10.1109\/TAC.2020.3013916","volume":"66","author":"P Jagtap","year":"2021","unstructured":"Jagtap, P., Soudjani, S., Zamani, M.: Formal synthesis of stochastic systems via control barrier certificates. IEEE Trans. Autom. Control 66(7), 3097\u20133110 (2021)","journal-title":"IEEE Trans. Autom. Control"},{"issue":"3\/4","key":"1_CR61","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1145\/2429135.2429155","volume":"46","author":"D Jovanovic","year":"2012","unstructured":"Jovanovic, D., de Moura, L.: Solving non-linear arithmetic. ACM Commun. Comput. Algebra 46(3\/4), 104\u2013105 (2012)","journal-title":"ACM Commun. Comput. Algebra"},{"key":"1_CR62","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. 6337, pp. 390\u2013406. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15769-1_24"},{"key":"1_CR63","doi-asserted-by":"crossref","unstructured":"Katoen, J., Zapreev, I.S., Hahn, E.M., Hermanns, H., Jansen, D.N.: The ins and outs of the probabilistic model checker MRMC. In: QEST, pp. 167\u2013176. IEEE Computer Society (2009)","DOI":"10.1109\/QEST.2009.11"},{"key":"1_CR64","unstructured":"Kiefer, S., Mayr, R., Shirmohammadi, M., Totzke, P., Wojtczak, D.: How to play in infinite mdps (invited talk). In: ICALP. LIPIcs, vol.\u00a0168, pp. 3:1\u20133:18. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2020)"},{"key":"1_CR65","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"567","DOI":"10.1007\/978-3-319-96145-3_30","volume-title":"Computer Aided Verification","author":"J K\u0159et\u00ednsk\u00fd","year":"2018","unstructured":"K\u0159et\u00ednsk\u00fd, J., Meggendorfer, T., Sickert, S., Ziegler, C.: Rabinizer 4: From LTL to your favourite deterministic automaton. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 567\u2013577. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_30"},{"issue":"1","key":"1_CR66","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1073\/pnas.53.1.8","volume":"53","author":"HJ Kushner","year":"1965","unstructured":"Kushner, H.J.: On the stability of stochastic dynamical systems. Proc. Natl. Acad. Sci. 53(1), 8\u201312 (1965)","journal-title":"Proc. Natl. Acad. Sci."},{"key":"1_CR67","unstructured":"Kushner, H.: Stochastic Stability and Control. Mathematics in science and engineering. Academic Press (1967)"},{"key":"1_CR68","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). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47"},{"issue":"1","key":"1_CR69","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(91)90030-6","volume":"94","author":"KG Larsen","year":"1991","unstructured":"Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. Inf. Comput. 94(1), 1\u201328 (1991)","journal-title":"Inf. Comput."},{"key":"1_CR70","doi-asserted-by":"crossref","unstructured":"Lavaei, A., Soudjani, S., Abate, A., Zamani, M.: Automated verification and synthesis of stochastic hybrid systems: a survey. In: Automatica, vol.\u00a0146 (2022)","DOI":"10.1016\/j.automatica.2022.110617"},{"key":"1_CR71","doi-asserted-by":"crossref","unstructured":"Lavaei, A., Soudjani, S., Frazzoli, E.: Safety barrier certificates for stochastic hybrid systems. In: ACC, pp. 880\u2013885. IEEE (2022)","DOI":"10.23919\/ACC53348.2022.9867754"},{"key":"1_CR72","doi-asserted-by":"crossref","unstructured":"Lechner, M., \u017dikeli\u0107, \u0110., Chatterjee, K., Henzinger, T.A.: Stability verification in stochastic control systems via neural network supermartingales. In: AAAI, pp. 7326\u20137336. AAAI Press (2022)","DOI":"10.1609\/aaai.v36i7.20695"},{"key":"1_CR73","doi-asserted-by":"crossref","unstructured":"Majumdar, R., Sathiyanarayana, V.R.: Sound and complete proof rules for probabilistic termination. Proc. ACM Program. Lang. 9(POPL), 1871\u20131902 (2025)","DOI":"10.1145\/3704899"},{"key":"1_CR74","doi-asserted-by":"publisher","first-page":"2703","DOI":"10.1109\/LCSYS.2024.3507279","volume":"8","author":"R Majumdar","year":"2024","unstructured":"Majumdar, R., Sathiyanarayana, V.R., Soudjani, S.: Necessary and sufficient certificates for almost sure reachability. IEEE Control. Syst. Lett. 8, 2703\u20132708 (2024)","journal-title":"IEEE Control. Syst. Lett."},{"key":"1_CR75","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems - Safety. Springer, Heidelberg (1995)","DOI":"10.1007\/978-1-4612-4222-2"},{"key":"1_CR76","doi-asserted-by":"publisher","first-page":"973","DOI":"10.1109\/LCSYS.2022.3229865","volume":"7","author":"FB Mathiesen","year":"2023","unstructured":"Mathiesen, F.B., Calvert, S.C., Laurenti, L.: Safety certification for stochastic systems via neural barrier functions. IEEE Control. Syst. Lett. 7, 973\u2013978 (2023)","journal-title":"IEEE Control. Syst. Lett."},{"key":"1_CR77","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), 33:1\u201333:28 (2018)","DOI":"10.1145\/3158121"},{"key":"1_CR78","series-title":"Cambridge Mathematical Library","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511626630","volume-title":"Markov Chains and Stochastic Stability","author":"S Meyn","year":"2009","unstructured":"Meyn, S., Tweedie, R.L.: Markov Chains and Stochastic Stability. Cambridge Mathematical Library, 2nd edn. Cambridge University Press, Cambridge (2009)","edition":"2"},{"key":"1_CR79","doi-asserted-by":"crossref","unstructured":"Moosbrugger, M., Bartocci, E., Katoen, J., Kov\u00e1cs, L.: Automated termination analysis of polynomial probabilistic programs. In: ESOP. Lecture Notes in Computer Science, vol. 12648, pp. 491\u2013518. Springer, Heidelberg (2021)","DOI":"10.1007\/978-3-030-72019-3_18"},{"key":"1_CR80","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"667","DOI":"10.1007\/978-3-030-90870-6_36","volume-title":"Formal Methods","author":"M Moosbrugger","year":"2021","unstructured":"Moosbrugger, M., Bartocci, E., Katoen, J.-P., Kov\u00e1cs, L.: The probabilistic termination tool amber. In: Huisman, M., P\u0103s\u0103reanu, C., Zhan, N. (eds.) FM 2021. LNCS, vol. 13047, pp. 667\u2013675. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-90870-6_36"},{"issue":"OOPSLA2","key":"1_CR81","doi-asserted-by":"publisher","first-page":"1497","DOI":"10.1145\/3563341","volume":"6","author":"M Moosbrugger","year":"2022","unstructured":"Moosbrugger, M., Stankovic, M., Bartocci, E., Kov\u00e1cs, L.: This is the moment for probabilistic loops. Proc. ACM Program. Lang. 6(OOPSLA2), 1497\u20131525 (2022)","journal-title":"Proc. ACM Program. Lang."},{"key":"1_CR82","unstructured":"Morgan, C.: Proof rules for probabilistic loops. In: Proceedings of the BCS-FACS 7th Conference on Refinement. p.\u00a010. FAC-RW\u201996, BCS Learning & Development Ltd., Swindon, GBR (1996)"},{"key":"1_CR83","doi-asserted-by":"crossref","unstructured":"Neustroev, G., Giacobbe, M., Lukina, A.: Neural continuous-time supermartingale certificates. In: AAAI. AAAI Press (2025)","DOI":"10.1609\/aaai.v39i26.34966"},{"key":"1_CR84","doi-asserted-by":"crossref","unstructured":"Nguyen, T., Kapur, D., Weimer, W., Forrest, S.: DIG: a dynamic invariant generator for polynomial and array invariants. ACM Trans. Softw. Eng. Methodol. 23(4), 30:1\u201330:30 (2014)","DOI":"10.1145\/2556782"},{"key":"1_CR85","doi-asserted-by":"crossref","unstructured":"Papachristodoulou, A., Prajna, S.: On the construction of Lyapunov functions using the sum of squares decomposition. In: CDC, pp. 3482\u20133487. IEEE (2002)","DOI":"10.1109\/CDC.2002.1184414"},{"key":"1_CR86","unstructured":"Parker, D.A.: Implementation of symbolic model checking for probabilistic systems. Ph.D. thesis, University of Birmingham, UK (2003)"},{"key":"1_CR87","unstructured":"Parrilo, P.A.: Structured semidefinite programs and semialgebraic geometry methods in robustness and optimization. California Institute of Technology (2000)"},{"key":"1_CR88","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: FOCS, pp. 46\u201357. IEEE Computer Society (1977)","DOI":"10.1109\/SFCS.1977.32"},{"issue":"1","key":"1_CR89","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/j.automatica.2005.08.007","volume":"42","author":"S Prajna","year":"2006","unstructured":"Prajna, S.: Barrier certificates for nonlinear model validation. Automatica (J. IFAC) 42(1), 117\u2013126 (2006)","journal-title":"Automatica (J. IFAC)"},{"key":"1_CR90","doi-asserted-by":"crossref","unstructured":"Prajna, S., Jadbabaie, A., Pappas, G.J.: Stochastic safety verification using barrier certificates. In: CDC, pp. 929\u2013934. IEEE (2004)","DOI":"10.1109\/CDC.2004.1428804"},{"issue":"8","key":"1_CR91","doi-asserted-by":"publisher","first-page":"1415","DOI":"10.1109\/TAC.2007.902736","volume":"52","author":"S Prajna","year":"2007","unstructured":"Prajna, S., Jadbabaie, A., Pappas, G.J.: A framework for worst-case and stochastic safety verification using barrier certificates. IEEE Trans. Autom. Control 52(8), 1415\u20131428 (2007)","journal-title":"IEEE Trans. Autom. Control"},{"key":"1_CR92","doi-asserted-by":"crossref","unstructured":"Safra, S.: On the complexity of omega-automata. In: FOCS, pp. 319\u2013327. IEEE Computer Society (1988)","DOI":"10.1109\/SFCS.1988.21948"},{"issue":"23","key":"1_CR93","doi-asserted-by":"publisher","first-page":"576","DOI":"10.3182\/20130904-3-FR-2041.00198","volume":"46","author":"S Sankaranarayanan","year":"2013","unstructured":"Sankaranarayanan, S., Chen, X., \u00c1brah\u00e1m, E.: Lyapunov function synthesis using handelman representations. IFAC Proc. Vol. 46(23), 576\u2013581 (2013)","journal-title":"IFAC Proc. Vol."},{"key":"1_CR94","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. 3148, pp. 53\u201368. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-27864-1_7"},{"key":"1_CR95","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1016\/j.jsc.2013.06.003","volume":"58","author":"Z She","year":"2013","unstructured":"She, Z., Li, H., Xue, B., Zheng, Z., Xia, B.: Discovering polynomial lyapunov functions for continuous dynamical systems. J. Symb. Comput. 58, 41\u201363 (2013)","journal-title":"J. Symb. Comput."},{"issue":"2","key":"1_CR96","doi-asserted-by":"publisher","first-page":"921","DOI":"10.1137\/120871456","volume":"12","author":"S Soudjani","year":"2012","unstructured":"Soudjani, S., Abate, A.: Adaptive and sequential gridding for abstraction and verification of stochastic processes. SIAM J. Appl. Dyn. Syst. 12(2), 921\u2013956 (2012)","journal-title":"SIAM J. Appl. Dyn. Syst."},{"key":"1_CR97","doi-asserted-by":"publisher","unstructured":"Sun, Y., Fu, H., Chatterjee, K., Goharshady, A.K.: Automated tail bound analysis for probabilistic recurrence relations. In: CAV (3). Lecture Notes in Computer Science, vol. 13966, pp. 16\u201339. Springer, Heidelberg (2023). https:\/\/doi.org\/10.1007\/978-3-031-37709-9_2","DOI":"10.1007\/978-3-031-37709-9_2"},{"key":"1_CR98","doi-asserted-by":"crossref","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)","DOI":"10.1145\/3450967"},{"key":"1_CR99","doi-asserted-by":"publisher","unstructured":"Takisaka, T., Zhang, L., Wang, C., Liu, J.: Lexicographic ranking supermartingales with lazy lower bounds. In: CAV (3). Lecture Notes in Computer Science, vol. 14683, pp. 420\u2013442. Springer, Heidelberg (2024). https:\/\/doi.org\/10.1007\/978-3-031-65633-0_19","DOI":"10.1007\/978-3-031-65633-0_19"},{"key":"1_CR100","doi-asserted-by":"publisher","unstructured":"Tarski, A.: A decision method for elementary algebra and geometry. In: Quantifier Elimination and Cylindrical Algebraic Decomposition, pp. 24\u201384. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/978-3-7091-9459-1_3","DOI":"10.1007\/978-3-7091-9459-1_3"},{"key":"1_CR101","doi-asserted-by":"crossref","unstructured":"Tkachev, I., Abate, A.: Formula-free finite abstractions for linear temporal verification of stochastic hybrid systems. In: HSCC, pp. 283\u2013292. ACM (2013)","DOI":"10.1145\/2461328.2461372"},{"key":"1_CR102","doi-asserted-by":"crossref","unstructured":"\u017dikeli\u0107, \u0110., Lechner, M., Henzinger, T.A., Chatterjee, K.: Learning control policies for stochastic systems with reach-avoid guarantees. In: AAAI, pp. 11926\u201311935. AAAI Press (2023)","DOI":"10.1609\/aaai.v37i10.26407"},{"key":"1_CR103","unstructured":"\u017dikeli\u0107, \u0110., Lechner, M., Verma, A., Chatterjee, K., Henzinger, T.A.: Compositional policy learning in stochastic control systems with formal guarantees. In: NeurIPS (2023)"},{"key":"1_CR104","doi-asserted-by":"crossref","unstructured":"Wang, D., Hoffmann, J., Reps, T.W.: Central moment analysis for cost accumulators in probabilistic programs. In: PLDI, pp. 559\u2013573. ACM (2021)","DOI":"10.1145\/3453483.3454062"},{"key":"1_CR105","doi-asserted-by":"crossref","unstructured":"Wang, J., Sun, Y., Fu, H., Chatterjee, K., Goharshady, A.K.: Quantitative analysis of assertion violations in probabilistic programs. In: PLDI, pp. 1171\u20131186. ACM (2021)","DOI":"10.1145\/3453483.3454102"},{"key":"1_CR106","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: PLDI, pp. 204\u2013220. ACM (2019)","DOI":"10.1145\/3314221.3314581"},{"key":"1_CR107","doi-asserted-by":"crossref","unstructured":"Wang, P., Yang, T., Fu, H., Li, G., Ong, C.L.: Static posterior inference of bayesian probabilistic programming via polynomial solving. Proc. ACM Program. Lang. 8(PLDI), 1361\u20131386 (2024)","DOI":"10.1145\/3656432"},{"issue":"6","key":"1_CR108","doi-asserted-by":"publisher","first-page":"572","DOI":"10.3166\/EJC.18.572-587","volume":"18","author":"L Zhang","year":"2012","unstructured":"Zhang, L., She, Z., Ratschan, S., Hermanns, H., Hahn, E.M.: Safety verification for probabilistic hybrid systems. Eur. J. Control. 18(6), 572\u2013587 (2012)","journal-title":"Eur. J. Control."},{"key":"1_CR109","doi-asserted-by":"publisher","unstructured":"Zhi, D., Wang, P., Liu, S., Ong, C.L., Zhang, M.: Unifying qualitative and quantitative safety verification of dnn-controlled systems. In: CAV (2). Lecture Notes in Computer Science, vol. 14682, pp. 401\u2013426. Springer, Heidelberg (2024). https:\/\/doi.org\/10.1007\/978-3-031-65630-9_20","DOI":"10.1007\/978-3-031-65630-9_20"},{"key":"1_CR110","doi-asserted-by":"crossref","unstructured":"Zikelic, D., Chang, B.E., Bolignano, P., Raimondi, F.: Differential cost analysis with simultaneous potentials and anti-potentials. In: PLDI, pp. 442\u2013457. ACM (2022)","DOI":"10.1145\/3519939.3523435"}],"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-98679-6_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,7]],"date-time":"2025-09-07T16:17:47Z","timestamp":1757261867000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-98679-6_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031986789","9783031986796"],"references-count":110,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-98679-6_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"22 July 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"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":"Zagreb","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Croatia","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"37","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conferences.i-cav.org\/2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}