{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T00:51:50Z","timestamp":1775868710213,"version":"3.50.1"},"publisher-location":"Cham","reference-count":71,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031711619","type":"print"},{"value":"9783031711626","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T00:00:00Z","timestamp":1726012800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T00:00:00Z","timestamp":1726012800000},"content-version":"vor","delay-in-days":0,"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><jats:p>We study the classical problem of verifying programs with respect to formal specifications given in the linear temporal logic (LTL). We first present novel sound and complete witnesses for LTL verification over imperative programs. Our witnesses are applicable to both verification (proving) and refutation (finding bugs) settings. We then consider LTL formulas in which atomic propositions can be polynomial constraints and turn our focus to polynomial arithmetic programs, i.e. programs in which every assignment and guard consists only of polynomial expressions. For this setting, we provide an efficient algorithm to automatically synthesize such LTL witnesses. Our synthesis procedure is both sound and semi-complete. Finally, we present experimental results demonstrating the effectiveness of our approach and that it can handle programs which were beyond the reach of previous state-of-the-art tools.<\/jats:p>","DOI":"10.1007\/978-3-031-71162-6_31","type":"book-chapter","created":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T02:02:27Z","timestamp":1725933747000},"page":"600-619","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Sound and\u00a0Complete Witnesses for\u00a0Template-Based Verification of\u00a0LTL Properties on\u00a0Polynomial Programs"],"prefix":"10.1007","author":[{"given":"Krishnendu","family":"Chatterjee","sequence":"first","affiliation":[]},{"given":"Amir","family":"Goharshady","sequence":"additional","affiliation":[]},{"given":"Ehsan","family":"Goharshady","sequence":"additional","affiliation":[]},{"given":"Mehrdad","family":"Karrabi","sequence":"additional","affiliation":[]},{"given":"\u0110or\u0111e","family":"\u017dikeli\u0107","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,9,11]]},"reference":[{"key":"31_CR1","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 (2021)","DOI":"10.1145\/3453483.3454076"},{"key":"31_CR2","unstructured":"Baier, C., Katoen, J.: Principles of Model Checking. MIT Press (2008)"},{"key":"31_CR3","doi-asserted-by":"crossref","unstructured":"Baresi, L., Kallehbasti, M.M.P., Rossi, M.: Efficient scalable verification of LTL specifications. In: ICSE (1), pp. 711\u2013721. IEEE Computer Society (2015)","DOI":"10.1109\/ICSE.2015.84"},{"key":"31_CR4","doi-asserted-by":"crossref","unstructured":"Bauch, P., Havel, V., Barnat, J.: LTL model checking of LLVM bitcode with symbolic data. In: MEMICS, pp. 47\u201359 (2014)","DOI":"10.1007\/978-3-319-14896-0_5"},{"key":"31_CR5","doi-asserted-by":"crossref","unstructured":"Beyer, D.: Progress on software verification: SV-COMP 2022. In: TACAS, pp. 375\u2013402 (2022)","DOI":"10.1007\/978-3-030-99527-0_20"},{"key":"31_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"294","DOI":"10.1007\/978-3-540-70545-1_27","volume-title":"Computer Aided Verification","author":"M Bofill","year":"2008","unstructured":"Bofill, M., Nieuwenhuis, R., Oliveras, A., Rodr\u00edguez-Carbonell, E., Rubio, A.: The barcelogic SMT solver. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 294\u2013298. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-70545-1_27"},{"issue":"2","key":"31_CR7","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/s10703-011-0111-7","volume":"38","author":"A Bouajjani","year":"2011","unstructured":"Bouajjani, A., Bozga, M., Habermehl, P., Iosif, R., Moro, P., Vojnar, T.: Programs with lists are counter automata. Formal Methods Syst. Des. 38(2), 158\u2013192 (2011)","journal-title":"Formal Methods Syst. Des."},{"key":"31_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1007\/978-3-662-49674-9_22","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Brockschmidt","year":"2016","unstructured":"Brockschmidt, M., Cook, B., Ishtiaq, S., Khlaaf, H., Piterman, N.: T2: temporal property verification. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 387\u2013393. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49674-9_22"},{"key":"31_CR9","doi-asserted-by":"crossref","unstructured":"B\u00fcchi, J.R.: Symposium on decision problems: on a decision method in restricted second order arithmetic. In: Studies in Logic and the Foundations of Mathematics, vol.\u00a044, pp. 1\u201311 (1966)","DOI":"10.1016\/S0049-237X(09)70564-6"},{"key":"31_CR10","doi-asserted-by":"crossref","unstructured":"Cai, Z., Farokhnia, S., Goharshady, A.K., Hitarth, S.: Asparagus: automated synthesis of parametric gas upper-bounds for smart contracts. In: OOPSLA (2023)","DOI":"10.1145\/3622829"},{"key":"31_CR11","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Fu, H., Goharshady, A.K.: Termination analysis of probabilistic programs through positivstellensatz\u2019s. In: CAV, pp. 3\u201322 (2016)","DOI":"10.1007\/978-3-319-41528-4_1"},{"key":"31_CR12","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Fu, H., Goharshady, A.K., Goharshady, E.K.: Polynomial invariant generation for non-deterministic recursive programs. In: PLDI, pp. 672\u2013687 (2020)","DOI":"10.1145\/3385412.3385969"},{"key":"31_CR13","doi-asserted-by":"crossref","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. arXiv preprint arXiv:2403.05386 (2024)","DOI":"10.1007\/978-3-031-71162-6_31"},{"key":"31_CR14","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Goharshady, A.K., Meggendorfer, T., Zikelic, D.: Quantitative bounds on resource usage of probabilistic programs. In: OOPSLA (2024)","DOI":"10.1145\/3649824"},{"key":"31_CR15","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Goharshady, A.K., Meggendorfer, T., Zikelic, D.: Sound and complete certificates for quantitative termination analysis of probabilistic programs. In: CAV, pp. 55\u201378 (2022)","DOI":"10.1007\/978-3-031-13185-1_4"},{"key":"31_CR16","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Goharshady, E.K., Novotn\u00fd, P., \u017dikeli\u0107, D.: Proving non-termination by program reversal. In: PLDI, pp. 1033\u20131048 (2021)","DOI":"10.1145\/3453483.3454093"},{"key":"31_CR17","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Goharshady, E.K., Novotn\u00fd, P., \u017dikeli\u0107, U.: Equivalence and similarity refutation for probabilistic programs (PLDI) (2024). https:\/\/doi.org\/10.1145\/3656462","DOI":"10.1145\/3656462"},{"key":"31_CR18","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Novotn\u00fd, P., \u017dikeli\u0107, D.: Stochastic invariants for probabilistic termination. In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, 18\u201320 January 2017, pp. 145\u2013160. ACM (2017). https:\/\/doi.org\/10.1145\/3009837.3009873","DOI":"10.1145\/3009837.3009873"},{"key":"31_CR19","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2022.104977","volume":"289","author":"A Cimatti","year":"2022","unstructured":"Cimatti, A., Griggio, A., Magnago, E.: LTL falsification in infinite-state systems. Inf. Comput. 289, 104977 (2022)","journal-title":"Inf. Comput."},{"key":"31_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"376","DOI":"10.1007\/978-3-030-25540-4_21","volume-title":"Computer Aided Verification","author":"A Cimatti","year":"2019","unstructured":"Cimatti, A., Griggio, A., Magnago, E., Roveri, M., Tonetta, S.: Extending nuXmv with timed transition systems and timed temporal properties. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 376\u2013386. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_21"},{"key":"31_CR21","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The mathsat5 SMT solver. In: TACAS, pp. 93\u2013107 (2013)","DOI":"10.1007\/978-3-642-36742-7_7"},{"key":"31_CR22","doi-asserted-by":"crossref","unstructured":"Clark, A.: Verification and synthesis of control barrier functions. In: CDC, pp. 6105\u20136112 (2021)","DOI":"10.1109\/CDC45484.2021.9683520"},{"key":"31_CR23","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: CAV (2000)","DOI":"10.1007\/10722167_15"},{"key":"31_CR24","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R.: Handbook of Model Checking. Springer (2018)","DOI":"10.1007\/978-3-319-10575-8"},{"key":"31_CR25","doi-asserted-by":"crossref","unstructured":"Col\u00f3n, M.A., Sankaranarayanan, S., Sipma, H.B.: Linear invariant generation using non-linear constraint solving. In: CAV, pp. 420\u2013432 (2003)","DOI":"10.1007\/978-3-540-45069-6_39"},{"key":"31_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"384","DOI":"10.1007\/978-3-662-46681-0_30","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"B Cook","year":"2015","unstructured":"Cook, B., Khlaaf, H., Piterman, N.: Fairness for infinite-state systems. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 384\u2013398. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_30"},{"key":"31_CR27","doi-asserted-by":"crossref","unstructured":"Cook, B., Koskinen, E.: Making prophecies with decision predicates. In: POPL, pp. 399\u2013410 (2011)","DOI":"10.1145\/1926385.1926431"},{"key":"31_CR28","doi-asserted-by":"crossref","unstructured":"Cook, B., Koskinen, E.: Reasoning about nondeterminism in programs. In: PLDI, pp. 219\u2013230 (2013)","DOI":"10.1145\/2499370.2491969"},{"key":"31_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/978-3-319-41528-4_15","volume-title":"Computer Aided Verification","author":"J Daniel","year":"2016","unstructured":"Daniel, J., Cimatti, A., Griggio, A., Tonetta, S., Mover, S.: Infinite-state liveness-to-safety via implicit abstraction and well-founded relations. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 271\u2013291. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_15"},{"issue":"5","key":"31_CR30","doi-asserted-by":"publisher","first-page":"822","DOI":"10.1090\/S0002-9939-1959-0113131-7","volume":"10","author":"L De Branges","year":"1959","unstructured":"De Branges, L.: The Stone-Weierstrass theorem. Proc. AMS 10(5), 822\u2013824 (1959)","journal-title":"Proc. AMS"},{"key":"31_CR31","doi-asserted-by":"crossref","unstructured":"Dietsch, D., Heizmann, M., Langenfeld, V., Podelski, A.: Fairness modulo theory: a new approach to LTL software model checking. In: CAV, pp. 49\u201366 (2015)","DOI":"10.1007\/978-3-319-21690-4_4"},{"issue":"124","key":"31_CR32","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. Journal f\u00fcr die reine und angewandte Mathematik 1902(124), 1\u201327 (1902)","journal-title":"Journal f\u00fcr die reine und angewandte Mathematik"},{"key":"31_CR33","doi-asserted-by":"crossref","unstructured":"Farzan, A., Kincaid, Z., Podelski, A.: Proving liveness of parameterized programs. In: LICS, pp. 185\u2013196 (2016)","DOI":"10.1145\/2933575.2935310"},{"key":"31_CR34","doi-asserted-by":"crossref","unstructured":"Feautrier, P., Gonnord, L.: Accelerated invariant generation for C programs with aspic and c2fsm. Electron. Notes Theor. Comput. Sci. 3\u201313 (2010)","DOI":"10.1016\/j.entcs.2010.09.014"},{"key":"31_CR35","doi-asserted-by":"crossref","unstructured":"Feng, Y., Zhang, L., Jansen, D.N., Zhan, N., Xia, B.: Finding polynomial loop invariants for probabilistic programs. In: ATVA, pp. 400\u2013416 (2017)","DOI":"10.1007\/978-3-319-68167-2_26"},{"key":"31_CR36","doi-asserted-by":"crossref","unstructured":"Floyd, R.W.: Assigning meanings to programs. In: Program Verification: Fundamental Issues in Computer Science, pp. 65\u201381 (1993)","DOI":"10.1007\/978-94-011-1793-7_4"},{"key":"31_CR37","unstructured":"Frohn, F., Giesl, J., Moser, G., Rubio, A., Yamada, A., et\u00a0al.: Termination competition 2022 (2021). https:\/\/termination-portal.org\/wiki\/Termination_Competition_2022"},{"key":"31_CR38","unstructured":"Fulton, N.: Verifiably safe autonomy for cyber-physical systems. Ph.D. thesis, Carnegie Mellon University (2018)"},{"key":"31_CR39","doi-asserted-by":"crossref","unstructured":"Funke, F., Jantsch, S., Baier, C.: Farkas certificates and minimal witnesses for probabilistic reachability constraints. In: TACAS, pp. 324\u2013345 (2020)","DOI":"10.1007\/978-3-030-45190-5_18"},{"key":"31_CR40","doi-asserted-by":"crossref","unstructured":"Graf, S., Sa\u00efdi, H.: Construction of abstract state graphs with PVS. In: CAV, pp. 72\u201383 (1997)","DOI":"10.1007\/3-540-63166-6_10"},{"key":"31_CR41","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Srivastava, S., Venkatesan, R.: Program analysis as constraint solving. In: PLDI, pp. 281\u2013292 (2008)","DOI":"10.1145\/1375581.1375616"},{"key":"31_CR42","doi-asserted-by":"crossref","unstructured":"Gurriet, T., Singletary, A., Reher, J., Ciarletta, L., Feron, E., Ames, A.D.: Towards a framework for realizable safety critical control through active set invariance. In: ICCPS, pp. 98\u2013106 (2018)","DOI":"10.1109\/ICCPS.2018.00018"},{"key":"31_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1007\/978-3-319-02444-8_26","volume-title":"Automated Technology for Verification and Analysis","author":"M Heizmann","year":"2013","unstructured":"Heizmann, M., Hoenicke, J., Leike, J., Podelski, A.: Linear ranking for linear Lasso programs. In: Van Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 365\u2013380. Springer, Cham (2013). https:\/\/doi.org\/10.1007\/978-3-319-02444-8_26"},{"key":"31_CR44","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":"31_CR45","doi-asserted-by":"crossref","unstructured":"Kincaid, Z., Cyphert, J., Breck, J., Reps, T.W.: Non-linear reasoning for invariant synthesis. In: POPL, pp. 54:1\u201354:33 (2018)","DOI":"10.1145\/3158142"},{"key":"31_CR46","doi-asserted-by":"crossref","unstructured":"Magill, S., Tsai, M., Lee, P., Tsay, Y.: Automatic numeric abstractions for heap-manipulating programs. In: POPL, pp. 211\u2013222 (2010)","DOI":"10.1145\/1707801.1706326"},{"key":"31_CR47","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: A hierarchy of temporal properties. In: PODC, pp. 377\u2013410 (1990)","DOI":"10.1145\/93385.93442"},{"key":"31_CR48","doi-asserted-by":"publisher","unstructured":"Meng, Y., Liu, J.: Lyapunov-barrier characterization of robust reach-avoid-stay specifications for hybrid systems (2022). https:\/\/doi.org\/10.48550\/ARXIV.2211.00814","DOI":"10.48550\/ARXIV.2211.00814"},{"key":"31_CR49","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"},{"key":"31_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"31_CR51","unstructured":"Neumann, E., Ouaknine, J., Worrell, J.: On ranking function synthesis and termination for polynomial programs. In: CONCUR, pp. 15:1\u201315:15 (2020)"},{"issue":"2","key":"31_CR52","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/s10703-021-00377-1","volume":"57","author":"O Padon","year":"2021","unstructured":"Padon, O., Hoenicke, J., McMillan, K.L., Podelski, A., Sagiv, M., Shoham, S.: Temporal prophecy for proving temporal properties of infinite-state systems. Formal Methods Syst. Des. 57(2), 246\u2013269 (2021)","journal-title":"Formal Methods Syst. Des."},{"key":"31_CR53","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: FOCS, pp. 46\u201357 (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"31_CR54","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/978-3-540-24622-0_20","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A Podelski","year":"2004","unstructured":"Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 239\u2013251. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24622-0_20"},{"key":"31_CR55","doi-asserted-by":"crossref","unstructured":"Podelski, A., Rybalchenko, A.: Transition predicate abstraction and fair termination. In: POPL, pp. 132\u2013144 (2005)","DOI":"10.1145\/1047659.1040317"},{"issue":"2","key":"31_CR56","doi-asserted-by":"publisher","first-page":"358","DOI":"10.1090\/S0002-9947-1953-0053041-6","volume":"74","author":"HG Rice","year":"1953","unstructured":"Rice, H.G.: Classes of recursively enumerable sets and their decision problems. Trans. AMS 74(2), 358\u2013366 (1953)","journal-title":"Trans. AMS"},{"key":"31_CR57","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan, S., Sipma, H., Manna, Z.: Non-linear loop invariant generation using gr\u00f6bner bases. In: POPL, pp. 318\u2013329 (2004)","DOI":"10.1145\/982962.964028"},{"key":"31_CR58","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"},{"issue":"2","key":"31_CR59","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1007\/s11424-013-1004-1","volume":"26","author":"L Shen","year":"2013","unstructured":"Shen, L., Wu, M., Yang, Z., Zeng, Z.: Generating exact nonlinear ranking functions by symbolic-numeric hybrid method. J. Syst. Sci. Complex. 26(2), 291\u2013301 (2013)","journal-title":"J. Syst. Sci. Complex."},{"key":"31_CR60","unstructured":"Strejcek, J.: Linear temporal logic: expressiveness and model checking. Ph.D. thesis, Masaryk University (2004)"},{"key":"31_CR61","doi-asserted-by":"crossref","unstructured":"Summers, S., Lygeros, J.: Verification of discrete time stochastic hybrid systems: a stochastic reach-avoid decision problem. Autom. 1951\u20131961 (2010)","DOI":"10.1016\/j.automatica.2010.08.006"},{"key":"31_CR62","doi-asserted-by":"crossref","unstructured":"Sun, Y., Fu, H., Chatterjee, K., Goharshady, A.K.: Automated tail bound analysis for probabilistic recurrence relations. In: CAV, pp. 16\u201339 (2023)","DOI":"10.1007\/978-3-031-37709-9_2"},{"key":"31_CR63","doi-asserted-by":"crossref","unstructured":"Takisaka, T., Oyabu, Y., Urabe, N., Hasuo, I.: Ranking and repulsing supermartingales for reachability in randomized programs. TOPLAS 43(2), 5:1\u20135:46 (2021)","DOI":"10.1145\/3450967"},{"key":"31_CR64","doi-asserted-by":"crossref","unstructured":"Turing, A.M.: On computable numbers, with an application to the entscheidungsproblem. J. Math. 58(345\u2013363), 5 (1936)","DOI":"10.1093\/oso\/9780198250791.003.0005"},{"key":"31_CR65","doi-asserted-by":"crossref","unstructured":"Unno, H., Terauchi, T., Gu, Y., Koskinen, E.: Modular primal-dual fixpoint logic solving for temporal verification. In: POPL, pp. 2111\u20132140 (2023)","DOI":"10.1145\/3571265"},{"key":"31_CR66","doi-asserted-by":"crossref","unstructured":"Unno, H., Terauchi, T., Koskinen, E.: Constraint-based relational verification. In: CAV, pp. 742\u2013766 (2021)","DOI":"10.1007\/978-3-030-81685-8_35"},{"key":"31_CR67","doi-asserted-by":"crossref","unstructured":"\u017dikeli\u0107, D., Lechner, M., Henzinger, T.A., Chatterjee, K.: Learning control policies for stochastic systems with reach-avoid guarantees. In: AAAI, pp. 11926\u201311935 (2023)","DOI":"10.1609\/aaai.v37i10.26407"},{"key":"31_CR68","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 (2021)","DOI":"10.1145\/3410310"},{"key":"31_CR69","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 (2019)","DOI":"10.1145\/3314221.3314581"},{"key":"31_CR70","doi-asserted-by":"crossref","unstructured":"Wang, Q., Chen, M., Xue, B., Zhan, N., Katoen, J.: Synthesizing invariant barrier certificates via difference-of-convex programming. In: CAV, pp. 443\u2013466 (2021)","DOI":"10.1007\/978-3-030-81685-8_21"},{"key":"31_CR71","doi-asserted-by":"crossref","unstructured":"Zhang, Y., Yang, Z., Lin, W., Zhu, H., Chen, X., Li, X.: Safety verification of nonlinear hybrid systems based on bilinear programming. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 37(11), 2768\u20132778 (2018)","DOI":"10.1109\/TCAD.2018.2858383"}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-71162-6_31","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,27]],"date-time":"2024-11-27T23:01:51Z","timestamp":1732748511000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-71162-6_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,9,11]]},"ISBN":["9783031711619","9783031711626"],"references-count":71,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-71162-6_31","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,9,11]]},"assertion":[{"value":"11 September 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Milan","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 September 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 September 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.fm24.polimi.it\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}