{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,25]],"date-time":"2025-10-25T22:35:37Z","timestamp":1761431737890,"version":"build-2065373602"},"publisher-location":"Cham","reference-count":45,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783032087065"},{"type":"electronic","value":"9783032087072"}],"license":[{"start":{"date-parts":[[2025,10,26]],"date-time":"2025-10-26T00:00:00Z","timestamp":1761436800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,10,26]],"date-time":"2025-10-26T00:00:00Z","timestamp":1761436800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-08707-2_19","type":"book-chapter","created":{"date-parts":[[2025,10,25]],"date-time":"2025-10-25T22:33:45Z","timestamp":1761431625000},"page":"411-424","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["PolyQEnt: A Polynomial Quantified Entailment Solver"],"prefix":"10.1007","author":[{"given":"Krishnendu","family":"Chatterjee","sequence":"first","affiliation":[]},{"given":"Amir Kafshdar","family":"Goharshady","sequence":"additional","affiliation":[]},{"given":"Ehsan Kafshdar","family":"Goharshady","sequence":"additional","affiliation":[]},{"given":"Mehrdad","family":"Karrabi","sequence":"additional","affiliation":[]},{"given":"Milad","family":"Saadat","sequence":"additional","affiliation":[]},{"given":"Maximilian","family":"Seeliger","sequence":"additional","affiliation":[]},{"given":"\u0110or\u0111e","family":"\u017dikeli\u0107","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,10,26]]},"reference":[{"issue":"4","key":"19_CR1","doi-asserted-by":"publisher","first-page":"709","DOI":"10.1007\/s11590-015-0894-3","volume":"10","author":"AA Ahmadi","year":"2016","unstructured":"Ahmadi, A.A., Majumdar, A.: Some applications of polynomial optimization in operations research and real-time decision making. Optim. Lett. 10(4), 709\u2013729 (2016)","journal-title":"Optim. Lett."},{"key":"19_CR2","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":"19_CR3","doi-asserted-by":"publisher","unstructured":"Barbosa, H., et al.: cvc5: a versatile and industrial-strength SMT solver. In: TACAS 2022. LNCS, vol. 13243, pp. 415\u2013442. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"19_CR4","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org (2016)"},{"key":"19_CR5","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":"19_CR6","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":"19_CR7","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. ACM (2020)","DOI":"10.1145\/3385412.3385969"},{"key":"19_CR8","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":"19_CR9","unstructured":"Chatterjee, K., et al.: Polyqent: a polynomial quantified entailment solver. arXiv preprint arXiv:2408.03796 (2024)"},{"key":"19_CR10","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Goharshady, E.K., Novotn\u00fd, P., Zikelic, D.: Proving non-termination by program reversal. In: PLDI, pp. 1033\u20131048. ACM (2021)","DOI":"10.1145\/3453483.3454093"},{"key":"19_CR11","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Novotn\u00fd, P., Zikelic, D.: Stochastic invariants for probabilistic termination. In: POPL, pp. 145\u2013160. ACM (2017)","DOI":"10.1145\/3009837.3009873"},{"key":"19_CR12","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The mathsat5 SMT solver. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 93\u2013107. Springer (2013)","DOI":"10.1007\/978-3-642-36742-7_7"},{"key":"19_CR13","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":"19_CR14","doi-asserted-by":"crossref","unstructured":"Col\u00f3n, M., Sipma, H.: Synthesis of linear ranking functions. In: TACAS. Lecture Notes in Computer Science, vol.\u00a02031, pp. 67\u201381. Springer (2001)","DOI":"10.1007\/3-540-45319-9_6"},{"key":"19_CR15","doi-asserted-by":"crossref","unstructured":"De\u00a0Moura, L., Bj\u00f8rner, N.: Z3: An efficient smt solver. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 337\u2013340. Springer (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"19_CR16","doi-asserted-by":"crossref","unstructured":"Dietsch, D., Heizmann, M., Hoenicke, J., Nutz, A., Podelski, A.: Ultimate treeautomizer (CHC-COMP tool description). In: HCVS\/PERR@ETAPS. EPTCS, vol.\u00a0296, pp. 42\u201347 (2019)","DOI":"10.4204\/EPTCS.296.7"},{"issue":"2","key":"19_CR17","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1145\/261320.261324","volume":"31","author":"A Dolzmann","year":"1997","unstructured":"Dolzmann, A., Sturm, T.: Redlog: computer algebra meets computer logic. ACM Sigsam Bulletin 31(2), 2\u20139 (1997)","journal-title":"ACM Sigsam Bulletin"},{"issue":"124","key":"19_CR18","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 (Crelles Journal) 1902(124), 1\u201327 (1902)","journal-title":"J. f\u00fcr die reine und angewandte Mathematik (Crelles Journal)"},{"key":"19_CR19","doi-asserted-by":"crossref","unstructured":"Fedyukovich, G., Prabhu, S., Madhukar, K., Gupta, A.: Solving constrained horn clauses using syntax and data. In: FMCAD, pp.\u00a01\u20139. IEEE (2018)","DOI":"10.23919\/FMCAD.2018.8603011"},{"key":"19_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1007\/978-3-030-25540-4_14","volume-title":"Computer Aided Verification","author":"G Fedyukovich","year":"2019","unstructured":"Fedyukovich, G., Prabhu, S., Madhukar, K., Gupta, A.: Quantified invariants via syntax-guided synthesis. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 259\u2013277. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_14"},{"key":"19_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"400","DOI":"10.1007\/978-3-319-68167-2_26","volume-title":"Automated Technology for Verification and Analysis","author":"Y Feng","year":"2017","unstructured":"Feng, Y., Zhang, L., Jansen, D.N., Zhan, N., Xia, B.: Finding polynomial loop invariants for probabilistic programs. In: D\u2019Souza, D., Narayan Kumar, K. (eds.) ATVA 2017. LNCS, vol. 10482, pp. 400\u2013416. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-68167-2_26"},{"key":"19_CR22","doi-asserted-by":"crossref","unstructured":"Floyd, R.W.: Assigning meanings to programs. In: Program Verification: Fundamental Issues in Computer Science, pp. 65\u201381. Springer (1993)","DOI":"10.1007\/978-94-011-1793-7_4"},{"key":"19_CR23","unstructured":"Frohn, F., Giesl, J., Moser, G., Rubio, A., Yamada, A., et\u00a0al.: Termination competition 2023 (2023). https:\/\/termination-portal.org\/wiki\/Termination_Competition_2023"},{"issue":"OOPSLA1","key":"19_CR24","doi-asserted-by":"publisher","first-page":"727","DOI":"10.1145\/3586052","volume":"7","author":"AK Goharshady","year":"2023","unstructured":"Goharshady, A.K., Hitarth, S., Mohammadi, F., Motwani, H.J.: Algebro-geometric algorithms for template-based synthesis of polynomial programs. Proc. ACM Program. Lang. 7(OOPSLA1), 727\u2013756 (2023)","journal-title":"Proc. ACM Program. Lang."},{"key":"19_CR25","doi-asserted-by":"crossref","unstructured":"Grebenshchikov, S., Lopes, N.P., Popeea, C., Rybalchenko, A.: Synthesizing software verifiers from proof rules. In: PLDI, pp. 405\u2013416. ACM (2012)","DOI":"10.1145\/2254064.2254112"},{"key":"19_CR26","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Jha, S., Tiwari, A., Venkatesan, R.: Synthesis of loop-free programs. In: PLDI, pp. 62\u201373. ACM (2011)","DOI":"10.1145\/1993498.1993506"},{"key":"19_CR27","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Srivastava, S., Venkatesan, R.: Program analysis as constraint solving. In: PLDI, pp. 281\u2013292. ACM (2008)","DOI":"10.1145\/1375581.1375616"},{"key":"19_CR28","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Zuleger, F.: The reachability-bound problem. In: PLDI, pp. 292\u2013304. ACM (2010)","DOI":"10.1145\/1806596.1806630"},{"key":"19_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/978-3-319-21690-4_20","volume-title":"Computer Aided Verification","author":"A Gurfinkel","year":"2015","unstructured":"Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The SeaHorn verification framework. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 343\u2013361. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_20"},{"issue":"1","key":"19_CR30","doi-asserted-by":"publisher","first-page":"35","DOI":"10.2140\/pjm.1988.132.35","volume":"132","author":"D Handelman","year":"1988","unstructured":"Handelman, D.: Representing polynomials by positive linear functions on compact convex Polyhedra. Pac. J. Math. 132(1), 35\u201362 (1988)","journal-title":"Pac. J. Math."},{"key":"19_CR31","doi-asserted-by":"crossref","unstructured":"Heizmann, M., Hoenicke, J., Leike, J., Podelski, A.: Linear ranking for linear lasso programs. CoRR abs\/1401.5347 (2014)","DOI":"10.1007\/978-3-319-02444-8_26"},{"key":"19_CR32","doi-asserted-by":"crossref","unstructured":"Hoffmann, J., Aehlig, K., Hofmann, M.: Multivariate amortized resource analysis. ACM Trans. Program. Lang. Syst. 34(3), 14:1\u201314:62 (2012)","DOI":"10.1145\/2362389.2362393"},{"key":"19_CR33","doi-asserted-by":"crossref","unstructured":"Hojjat, H., R\u00fcmmer, P.: The ELDARICA horn solver. In: FMCAD, pp.\u00a01\u20137. IEEE (2018)","DOI":"10.23919\/FMCAD.2018.8603013"},{"issue":"3","key":"19_CR34","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/s10703-016-0249-4","volume":"48","author":"A Komuravelli","year":"2016","unstructured":"Komuravelli, A., Gurfinkel, A., Chaki, S.: SMT-based model checking for recursive programs. Formal Methods Syst. Des. 48(3), 175\u2013205 (2016)","journal-title":"Formal Methods Syst. Des."},{"key":"19_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-030-17465-1_8","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Kura","year":"2019","unstructured":"Kura, S., Urabe, N., Hasuo, I.: Tail probabilities for randomized program runtimes via martingales for higher moments. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11428, pp. 135\u2013153. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17465-1_8"},{"key":"19_CR36","unstructured":"Matou\u0161ek, J., G\u00e4rtner, B.: Understanding and using linear programming, vol.\u00a01. Springer (2007)"},{"key":"19_CR37","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":"19_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1007\/978-3-540-24743-2_32","volume-title":"Hybrid Systems: Computation and Control","author":"S Prajna","year":"2004","unstructured":"Prajna, S., Jadbabaie, A.: Safety verification of hybrid systems using barrier certificates. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 477\u2013492. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24743-2_32"},{"key":"19_CR39","doi-asserted-by":"crossref","unstructured":"Prajna, S., Papachristodoulou, A., Parrilo, P.A.: Introducing sostools: a general purpose sum of squares programming solver. In: Proceedings of the 41st IEEE Conference on Decision and Control, 2002, vol.\u00a01, pp. 741\u2013746. IEEE (2002)","DOI":"10.1109\/CDC.2002.1184594"},{"issue":"3","key":"19_CR40","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":"19_CR41","doi-asserted-by":"publisher","unstructured":"Renegar, J.: On the computational complexity and geometry of the first-order theory of the reals. part iii: Quantifier elimination. J. Symbolic Comput. 13(3), 329\u2013352 (1992).https:\/\/doi.org\/10.1016\/S0747-7171(10)80005-7","DOI":"10.1016\/S0747-7171(10)80005-7"},{"issue":"5\u20136","key":"19_CR42","doi-asserted-by":"publisher","first-page":"497","DOI":"10.1007\/s10009-012-0223-4","volume":"15","author":"S Srivastava","year":"2013","unstructured":"Srivastava, S., Gulwani, S., Foster, J.S.: Template-based program verification and program synthesis. Int. J. Softw. Tools Technol. Transf. 15(5\u20136), 497\u2013518 (2013)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"19_CR43","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":"19_CR44","unstructured":"Wolfram, S.: The Mathematica Book. Inc. Wolfram Research, Champaign (2003)"},{"key":"19_CR45","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","Automated Technology for Verification and Analysis"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-08707-2_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,25]],"date-time":"2025-10-25T22:33:52Z","timestamp":1761431632000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-08707-2_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,26]]},"ISBN":["9783032087065","9783032087072"],"references-count":45,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-08707-2_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025,10,26]]},"assertion":[{"value":"26 October 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":"ATVA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Automated Technology for Verification and Analysis","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Bengaluru","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"India","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":"27 October 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31 October 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"atva2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/atva-2025","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}