{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,24]],"date-time":"2025-03-24T04:12:33Z","timestamp":1742789553987,"version":"3.40.2"},"reference-count":107,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2025,1,25]],"date-time":"2025-01-25T00:00:00Z","timestamp":1737763200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,1,25]],"date-time":"2025-01-25T00:00:00Z","timestamp":1737763200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/100009117","name":"Technische Universit\u00e4t Chemnitz","doi-asserted-by":"crossref","id":[{"id":"10.13039\/100009117","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2025,3]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>We provide a computer-assisted approach to ensure that a given discrete-time polynomial system is (asymptotically) stable. Our framework relies on constructive analysis together with formally certified sums of squares Lyapunov functions. The crucial steps are formalized within the proof assistant <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$\\texttt {Minlog}$$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>Minlog<\/mml:mi>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>. We illustrate our approach with an example issued from the control system literature.<\/jats:p>","DOI":"10.1007\/s10817-024-09717-2","type":"journal-article","created":{"date-parts":[[2025,1,25]],"date-time":"2025-01-25T07:21:50Z","timestamp":1737789710000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Computer-Assisted Proofs for Lyapunov Stability via Sums of Squares Certificates and Constructive Analysis"],"prefix":"10.1007","volume":"69","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2787-128X","authenticated-orcid":false,"given":"Grigory","family":"Devadze","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1147-3738","authenticated-orcid":false,"given":"Victor","family":"Magron","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3398-1226","authenticated-orcid":false,"given":"Stefan","family":"Streif","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,1,25]]},"reference":[{"key":"9717_CR1","doi-asserted-by":"crossref","unstructured":"Ahmed, D., Peruffo, A., Abate, A.: Automated and sound synthesis of lyapunov functions with SMT solvers. In Tools and Algorithms for the Construction and Analysis of Systems: 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, 2020, Proceedings, Part I 26, pp 97\u2013114. Springer (2020)","DOI":"10.1007\/978-3-030-45190-5_6"},{"key":"9717_CR2","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1007\/978-3-319-22102-1_3","volume-title":"International Conference on Interactive Theorem Proving","author":"A Anand","year":"2015","unstructured":"Anand, A., Knepper, R.: ROSCoq: robots powered by constructive reals. In: International Conference on Interactive Theorem Proving, pp. 34\u201350. Springer, Berlin (2015)"},{"key":"9717_CR3","doi-asserted-by":"crossref","unstructured":"Araiza-Illan, D., Eder, K., Richards, A.: Formal verification of control systems\u2019 properties with theorem proving. In Proceedings 2014 UKACC International Conference Control, pp 244\u2013249 (2014)","DOI":"10.1109\/CONTROL.2014.6915147"},{"key":"9717_CR4","doi-asserted-by":"crossref","unstructured":"Araiza-Illan, D., Eder, K., Richards, A.: Verification of control systems implemented in simulink with assertion checks and theorem proving: a case study. In Proceedings 2015 European Control Conference (ECC), pp 2670\u20132675 (2015)","DOI":"10.1109\/ECC.2015.7330941"},{"key":"9717_CR5","volume-title":"Foundations of Constructive Mathematics: Metamathematical Studies","author":"MJ Beeson","year":"1980","unstructured":"Beeson, M.J.: Foundations of Constructive Mathematics: Metamathematical Studies, vol. 6. Springer, Berlin (1980)"},{"key":"9717_CR6","doi-asserted-by":"crossref","unstructured":"Berger, U., Benl, H., Seisenberger, M., Schwichtenberg, H., Zuber: Proof Theory at Work: Program Development in the Minlog System. Springer, Dordrechtpp. pp 41\u201371 (1998)","DOI":"10.1007\/978-94-017-0435-9_2"},{"key":"9717_CR7","doi-asserted-by":"crossref","unstructured":"Berger, U., Benl, H., Seisenberger, M., Schwichtenberg, H., Zuber: Proof Theory at Work: Program Development in the Minlog System. Springer, Dordrechtpp. pp 41\u201371 (1998)","DOI":"10.1007\/978-94-017-0435-9_2"},{"issue":"3","key":"9717_CR8","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/s00224-011-9325-8","volume":"51","author":"U Berger","year":"2012","unstructured":"Berger, U., Seisenberger, M.: Proofs, programs, processes. Theory of Computing Systems 51(3), 313\u2013329 (2012)","journal-title":"Theory of Computing Systems"},{"key":"9717_CR9","doi-asserted-by":"publisher","first-page":"393","DOI":"10.1007\/978-3-642-22944-2_29","volume-title":"International Conference on Algebra and Coalgebra in Computer Science","author":"U Berger","year":"2011","unstructured":"Berger, U., Miyamoto, K., Schwichtenberg, H., Seisenberger, M.: Minlog-a tool for program extraction supporting algebras and coalgebras. In: International Conference on Algebra and Coalgebra in Computer Science, pp. 393\u2013399. Springer, Berlin (2011)"},{"key":"9717_CR10","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-61667-9","volume-title":"Constructive Analysis","author":"E Bishop","year":"1985","unstructured":"Bishop, E., Bridges, D.: Constructive Analysis, vol. 279. Springer, Berlin (1985)"},{"key":"9717_CR11","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1007\/BF00941398","volume":"71","author":"F Blanchini","year":"1991","unstructured":"Blanchini, F.: Constrained control for uncertain linear systems. J. Optim. Theor. Appl. 71, 465\u2013484 (1991)","journal-title":"J. Optim. Theor. Appl."},{"key":"9717_CR12","unstructured":"Bobot, F., Filli\u00e2tre, J.-C., March\u00e9, C., Melquiond, G., Paskevich, A.: The Why3 platform. LRI, CNRS & University Paris-Sud & INRIA Saclay, version 0.64 edition (2011)"},{"issue":"4","key":"9717_CR13","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/s10817-012-9255-4","volume":"50","author":"S Boldo","year":"2013","unstructured":"Boldo, S., Cl\u00e9ment, F., Filli\u00e2tre, J.-C., Mayero, M., Melquiond, G., Weis, P.: Wave equation numerical resolution: a comprehensive mechanized proof of a C program. J. Autom. Reason. 50(4), 423\u2013456 (2013)","journal-title":"J. Autom. Reason."},{"issue":"7","key":"9717_CR14","doi-asserted-by":"publisher","first-page":"1196","DOI":"10.1017\/S0960129514000437","volume":"26","author":"S Boldo","year":"2016","unstructured":"Boldo, S., Lelay, C., Melquiond, G.: Formalization of real analysis: a survey of proof assistants and libraries. Math. Struct. Comput. Sci. 26(7), 1196\u20131233 (2016)","journal-title":"Math. Struct. Comput. Sci."},{"key":"9717_CR15","doi-asserted-by":"crossref","unstructured":"Boyd, S., El Ghaoui, L., Feron, E., Balakrishnan, V.: Linear matrix inequalities in system and control theory. Stud. Appl. Math. 15 (1994)","DOI":"10.1137\/1.9781611970777"},{"key":"9717_CR16","volume-title":"Handbook of proof theory","author":"SR Buss","year":"1998","unstructured":"Buss, S.R.: Handbook of proof theory, vol. 137. Elsevier, Amsterdam (1998)"},{"issue":"16","key":"9717_CR17","doi-asserted-by":"publisher","first-page":"1523","DOI":"10.1016\/j.tcs.2010.11.052","volume":"412","author":"S Chevillard","year":"2011","unstructured":"Chevillard, S., Harrison, J., Joldes, M., Lauter, C.: Efficient and accurate computation of upper bounds of approximation errors. Theoret. Comput. Sci. 412(16), 1523\u20131543 (2011)","journal-title":"Theoret. Comput. Sci."},{"key":"9717_CR18","unstructured":"Cohen, C., Rouhling, D.: A formal proof of lasalle\u2019s invariance principle. https:\/\/github.com\/drouhling\/LaSalle (2019)"},{"key":"9717_CR19","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/978-3-319-66107-0_10","volume-title":"International Conference on Interactive Theorem Proving","author":"C Cohen","year":"2017","unstructured":"Cohen, C., Rouhling, D.: A formal proof in Coq of Lasalle\u2019s invariance principle. In: International Conference on Interactive Theorem Proving, pp. 148\u2013163. Springer, Berlin (2017)"},{"key":"9717_CR20","doi-asserted-by":"crossref","unstructured":"Cruz-Filipe, L., Geuvers, H., Wiedijk, F.: C-CoRN, the constructive Coq repository at Nijmegen. In: International Conference on Mathematical Knowledge Management, pp. 88\u2013103. Springer, Berlin (2004)","DOI":"10.1007\/978-3-540-27818-4_7"},{"key":"9717_CR21","doi-asserted-by":"crossref","unstructured":"Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-c. In: International Conference on Software Engineering and Formal Methods, pp. 233\u2013247. Springer, Berlin (2012)","DOI":"10.1007\/978-3-642-33826-7_16"},{"key":"9717_CR22","unstructured":"Dunford, N., J., Schwartz, J.T., W. G., Bade, Bartle, R.G.: Linear Operators. Wiley, New York (1971)"},{"key":"9717_CR23","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/3-540-44659-1_10","volume-title":"International Conference on Theorem Proving in Higher Order Logics","author":"JD Fleuriot","year":"2000","unstructured":"Fleuriot, J.D.: On the mechanization of real analysis in Isabelle\/HOL. In: International Conference on Theorem Proving in Higher Order Logics, pp. 145\u2013161. Springer, Berlin (2000)"},{"issue":"4","key":"9717_CR24","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1023\/A:1011908113514","volume":"27","author":"RA Gamboa","year":"2001","unstructured":"Gamboa, R.A., Kaufmann, M.: Nonstandard analysis in ACL2. J. Autom. Reason. 27(4), 323\u2013351 (2001)","journal-title":"J. Autom. Reason."},{"key":"9717_CR25","first-page":"79","volume-title":"International Workshop on Types for Proofs and Programs","author":"H Geuvers","year":"2000","unstructured":"Geuvers, H., Niqui, M.: Constructive reals in Coq: axioms and categoricity. In: International Workshop on Types for Proofs and Programs, pp. 79\u201395. Springer, Berlin (2000)"},{"issue":"8","key":"9717_CR26","doi-asserted-by":"publisher","first-page":"2291","DOI":"10.3934\/dcdsb.2015.20.2291","volume":"20","author":"P Giesl","year":"2015","unstructured":"Giesl, P., Hafstein, S.: Review on computational methods for Lyapunov functions. Discrete Contin. Dyn. Syst. Ser. B 20(8), 2291\u20132331 (2015)","journal-title":"Discrete Contin. Dyn. Syst. Ser. B"},{"key":"9717_CR27","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/978-3-642-39634-2_14","volume-title":"International Conference on Interactive Theorem Proving","author":"G Gonthier","year":"2013","unstructured":"Gonthier, G., Asperti, A., Avigad, J., Bertot, Y., Cohen, C., Garillot, F., Roux, L., St\u00e9phane, M., Assia, O.C., Russell, B., Ould, S., et al.: A machine-checked proof of the odd order theorem. In: International Conference on Interactive Theorem Proving, pp. 163\u2013179. Springer, Berlin (2013)"},{"key":"9717_CR28","unstructured":"Grigory, D.: con2formlog . https:\/\/www.tu-chemnitz.de\/etit\/control\/research\/formal\/index.php.en (2020). Accessed 10 Oct 2022"},{"key":"9717_CR29","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/j.orl.2008.10.003","volume":"37","author":"N Gvozdenovic","year":"2009","unstructured":"Gvozdenovic, N., Laurent, M., Vallentin, F.: Block-diagonal semidefinite programming hierarchies for 0\/1 programming. Oper. Res. Lett. 37, 27\u201331 (2009)","journal-title":"Oper. Res. Lett."},{"key":"9717_CR30","doi-asserted-by":"publisher","DOI":"10.1201\/9781482283280","volume-title":"Stability and stable oscillations in discrete time systems","author":"A Halanay","year":"2000","unstructured":"Halanay, A., Rasvan, V.: Stability and stable oscillations in discrete time systems, vol. 2. CRC Press, Baco Raton (2000)"},{"key":"9717_CR31","doi-asserted-by":"crossref","unstructured":"Hales, T., Adams, M., Bauer, G., Dat, D.T., Harrison, J., Hoang, L.T., Kaliszyk, C., Magron, V., Mclaughlin, S., Nguyen, T.T., Nguyen, Q.T., Nipkow, T., Obua, S., Pleso, J., Rute, J., Solovyev, A., Ta, T.H.A., Tran, N.T., Trieu, T.D., Urban, J., Vu, K.K., Zumkeller, R.: A formal proof of the kepler conjecture. Forum Math. Pi. 5 (2017)","DOI":"10.1017\/fmp.2017.1"},{"key":"9717_CR32","doi-asserted-by":"crossref","unstructured":"Hales, T., Adams, M., Bauer, G., Dat, D.T., Harrison, J., Hoang, L.T., Kaliszyk, C., Magron, V., Mclaughlin, S., Nguyen, T.T., Nguyen, Q.T., Nipkow, T., Obua, S., Pleso, J., Rute, J., Solovyev, A., Ta, T.H.A., Tran, N.T., Trieu, T.D., Urban, J., Vu, K.K., Zumkeller, R.: A formal proof of the kepler conjecture. Forum Math. Pi. 5 (2017)","DOI":"10.1017\/fmp.2017.1"},{"key":"9717_CR33","first-page":"265","volume-title":"International Conference on Formal Methods in Computer-Aided Design","author":"J Harrison","year":"1996","unstructured":"Harrison, J.: HOL light: a tutorial introduction. In: International Conference on Formal Methods in Computer-Aided Design, pp. 265\u2013269. Springer, Berlin (1996)"},{"key":"9717_CR34","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/978-3-540-74591-4_9","volume-title":"International Conference on Theorem Proving in Higher Order Logics","author":"J Harrison","year":"2007","unstructured":"Harrison, J.: Verifying nonlinear real formulas via sums of squares. In: International Conference on Theorem Proving in Higher Order Logics, pp. 102\u2013118. Springer, Berlin (2007)"},{"key":"9717_CR35","volume-title":"Theorem proving with the real numbers","author":"J Harrison","year":"2012","unstructured":"Harrison, J.: Theorem proving with the real numbers. Springer, Berlin (2012)"},{"key":"9717_CR36","doi-asserted-by":"crossref","unstructured":"Immler, F., Tan, Y.K.: The poincar\u00e9-bendixson theorem in isabelle\/hol. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, pp. 338-352, New York. Association for Computing Machinery (2020)","DOI":"10.1145\/3372885.3373833"},{"issue":"1\u20134","key":"9717_CR37","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/s10817-017-9448-y","volume":"61","author":"F Immler","year":"2018","unstructured":"Immler, F.: A verified ODE solver and the Lorenz attractor. J. Autom. Reason. 61(1\u20134), 73\u2013111 (2018)","journal-title":"J. Autom. Reason."},{"issue":"2","key":"9717_CR38","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1007\/s10817-018-9449-5","volume":"62","author":"F Immler","year":"2019","unstructured":"Immler, F., Traut, C.: The flow of ODEs: formalization of variational equation and Poincar\u00e9 map. J. Autom. Reason. 62(2), 215\u2013236 (2019)","journal-title":"J. Autom. Reason."},{"key":"9717_CR39","first-page":"01","volume":"1381","author":"H Ishihara","year":"2004","unstructured":"Ishihara, H.: Informal constructive reverse mathematics. S\u016brikaisekikenky\u016bsho K\u014dky\u016broku. 1381, 01 (2004)","journal-title":"S\u016brikaisekikenky\u016bsho K\u014dky\u016broku."},{"issue":"6","key":"9717_CR40","doi-asserted-by":"publisher","first-page":"857","DOI":"10.1016\/S0005-1098(01)00028-0","volume":"37","author":"Z-P Jiang","year":"2001","unstructured":"Jiang, Z.-P., Wang, Y.: Input-to-state stability for discrete-time nonlinear systems. Automatica 37(6), 857\u2013869 (2001)","journal-title":"Automatica"},{"key":"9717_CR41","doi-asserted-by":"crossref","unstructured":"Kaltofen, E.\u00a0L., Li, B., Yang, Z., Zhi, L.: Exact certification of global optimality of approximate factorizations via rationalizing sums-of-squares with floating point scalars. In Proceedings of the 21st International Symposium on Symbolic and Algebraic computation, ISSAC \u201908, pp. 155\u2013164, New York. ACM (2008)","DOI":"10.1145\/1390768.1390792"},{"key":"9717_CR42","unstructured":"Khalil, H.\u00a0K.: Nonlinear systems. Upper Saddle River (2002)"},{"key":"9717_CR43","doi-asserted-by":"crossref","unstructured":"Ko, Ker-I: Computational Complexity of Real Functions. pp 40\u201370. Birkh\u00e4user Boston (1991)","DOI":"10.1007\/978-1-4684-6802-1_3"},{"key":"9717_CR44","unstructured":"Konecny, Michal, Steinberg, Florian, Thies, Holger: Computable Analysis for Verified Exact Real Computation. In: Nitin, S., Sunil, S (eds), 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020), Volume 182 of Leibniz International Proceedings in Informatics (LIPIcs), Dagstuhl. pp. 50:1\u201350:18. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik (2020)"},{"key":"9717_CR45","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/978-3-030-88853-4_16","volume-title":"Logic, Language, Information, and Computation","author":"M Konecny","year":"2021","unstructured":"Konecny, M., Park, S., Thies, H.: Axiomatic reals and certified efficient exact real computation. In: Silva, A., Wassermann, R., de Queiroz, R. (eds.) Logic, Language, Information, and Computation, pp. 252\u2013268. Springer, Cham (2021)"},{"issue":"1:1","key":"9717_CR46","first-page":"1","volume":"9","author":"R Krebbers","year":"2013","unstructured":"Krebbers, R., Spitters, B.: Type classes for efficient exact real arithmetic in Coq. Logical Methods Comput. Sci. 9(1:1), 1\u201327 (2013)","journal-title":"Logical Methods Comput. Sci."},{"key":"9717_CR47","volume-title":"Nonlinear Adaptive Control Des.","author":"M Krstic","year":"1995","unstructured":"Krstic, M., Kokotovic, P.V., Kanellakopoulos, I.: Nonlinear Adaptive Control Des., 1st edn. Wiley, USA (1995)","edition":"1"},{"issue":"1\u20132","key":"9717_CR48","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1016\/S0304-3975(98)00291-6","volume":"219","author":"BA Kushner","year":"1999","unstructured":"Kushner, B.A.: Markov\u2019s constructive analysis; a participant\u2019s view. Theoret. Comput. Sci. 219(1\u20132), 267\u2013285 (1999)","journal-title":"Theoret. Comput. Sci."},{"key":"9717_CR49","doi-asserted-by":"publisher","DOI":"10.1201\/9780203910290","volume-title":"Theory of difference equations numerical methods and applications","author":"V Lakshmikantham","year":"2002","unstructured":"Lakshmikantham, V., Trigiante, V.: Theory of difference equations numerical methods and applications. CRC Press, Baco Raton (2002)"},{"key":"9717_CR50","doi-asserted-by":"crossref","unstructured":"Lasserre,\u00a0J.B.: Moments, positive polynomials and their applications, Vol.\u00a01. World Scientific (2009)","DOI":"10.1142\/p665"},{"issue":"3","key":"9717_CR51","doi-asserted-by":"publisher","first-page":"796","DOI":"10.1137\/S1052623400366802","volume":"11","author":"JB Lasserre","year":"2001","unstructured":"Lasserre, J.B.: Global optimization with polynomials and the problem of moments. SIAM J. Optim. 11(3), 796\u2013817 (2001)","journal-title":"SIAM J. Optim."},{"issue":"4","key":"9717_CR52","doi-asserted-by":"publisher","first-page":"1643","DOI":"10.1137\/070685051","volume":"47","author":"JB Lasserre","year":"2008","unstructured":"Lasserre, J.B., Henrion, D., Prieur, C., Tr\u00e9lat, E.: Nonlinear optimal control via occupation measures and LMI-relaxations. SIAM J. Control. Optim. 47(4), 1643\u20131666 (2008)","journal-title":"SIAM J. Control. Optim."},{"key":"9717_CR53","doi-asserted-by":"crossref","unstructured":"Lawrence, Andrew, Berger, Ulrich, Seisenberger, Monika: Extracting a DPLL algorithm. Electronic Notes in Theoretical Computer Science 286, 243\u2013256. Proceedings of the 28th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXVIII) (2012)","DOI":"10.1016\/j.entcs.2012.08.016"},{"key":"9717_CR54","doi-asserted-by":"crossref","unstructured":"Magron, Victor, Safey El\u00a0Din, Mohab: On Exact Polya and Putinar\u2019s Representations. In Proceedings of the 2018 ACM International Symposium on Symbolic and Algebraic Computation, pp. 279\u2013286 (2018)","DOI":"10.1145\/3208976.3208986"},{"key":"9717_CR55","doi-asserted-by":"crossref","unstructured":"Magron, V., Seidler, H., de\u00a0Wolff, T.: Exact optimization via sums of nonnegative circuits and arithmetic-geometric-mean-exponentials. In Proceedings of the 2019 on International Symposium on Symbolic and Algebraic Computation, pp. 291\u2013298 (2019)","DOI":"10.1145\/3326229.3326271"},{"issue":"2","key":"9717_CR56","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1145\/3282678.3282681","volume":"52","author":"V Magron","year":"2018","unstructured":"Magron, V., Din, M.S.E.: Realcertify: a Maple package for certifying non-negativity. ACM Commun. Comput. Algebra 52(2), 34\u201337 (2018)","journal-title":"ACM Commun. Comput. Algebra"},{"key":"9717_CR57","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1016\/j.jsc.2022.08.002","volume":"115","author":"V Magron","year":"2023","unstructured":"Magron, V., Wang, J.: Sonc optimization and exact nonnegativity certificates via second-order cone programming. J. Symb. Comput. 115, 346\u2013370 (2023)","journal-title":"J. Symb. Comput."},{"issue":"1","key":"9717_CR58","first-page":"1","volume":"8","author":"V Magron","year":"2015","unstructured":"Magron, V., Allamigeon, X., Gaubert, S., Werner, B.: Formal proofs for nonlinear optimization. J. rmalized Reason. 8(1), 1\u201324 (2015)","journal-title":"J. rmalized Reason."},{"issue":"1531\u20133492\u20132019\u2013","key":"9717_CR59","first-page":"6745","volume":"24","author":"V Magron","year":"2019","unstructured":"Magron, V., Forets, M., Henrion, D.: Semidefinite approximations of invariant measures for polynomial systems. Discrete Contin.Dyn. yst.B 24(1531\u20133492\u20132019\u201312\u20136745), 6745 (2019)","journal-title":"Discrete Contin.Dyn. yst.B"},{"key":"9717_CR60","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1016\/j.jsc.2018.06.005","volume":"93","author":"V Magron","year":"2019","unstructured":"Magron, V., Din, M.S.E., Schweighofer, M.: Algorithms for weighted sum of squares decomposition of non-negative univariate polynomials. J. Symb. Comput. 93, 200\u2013220 (2019)","journal-title":"J. Symb. Comput."},{"issue":"4","key":"9717_CR61","doi-asserted-by":"publisher","first-page":"2799","DOI":"10.1137\/17M1121044","volume":"57","author":"V Magron","year":"2019","unstructured":"Magron, V., Garoche, P.-L., Henrion, D., Thirioux, X.: Semidefinite approximations of reachable sets for discrete-time polynomial systems. SIAM J. Control. Optim. 57(4), 2799\u20132820 (2019)","journal-title":"SIAM J. Control. Optim."},{"key":"9717_CR62","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1007\/978-3-642-39634-2_34","volume-title":"International Conference on Interactive Theorem Proving","author":"E Makarov","year":"2013","unstructured":"Makarov, E., Spitters, B.: The Picard algorithm for ordinary differential equations in Coq. In: International Conference on Interactive Theorem Proving, pp. 463\u2013468. Springer, Berlin (2013)"},{"key":"9717_CR63","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-84882-535-2","volume-title":"Constructions of strict Lyapunov functions","author":"M Malisoff","year":"2009","unstructured":"Malisoff, M., Mazenc, F.: Constructions of strict Lyapunov functions. Springer, Berlin (2009)"},{"issue":"2","key":"9717_CR64","doi-asserted-by":"publisher","first-page":"413","DOI":"10.2140\/pjm.1982.99.413","volume":"99","author":"M Mandelker","year":"1982","unstructured":"Mandelker, M.: Continuity of monotone functions. Pac. J. Math. 99(2), 413\u2013418 (1982)","journal-title":"Pac. J. Math."},{"key":"9717_CR65","doi-asserted-by":"crossref","unstructured":"Mandelkern, Mark: Constructive continuity. Am. Math. Soc. 277 (1983)","DOI":"10.1090\/memo\/0277"},{"key":"9717_CR66","first-page":"103","volume":"58","author":"C Man-Duen","year":"1995","unstructured":"Man-Duen, C., Lam, T.Y., Reznick, B.: Sums of squares of real polynomials. Proc. Symposia Pure Math. 58, 103\u2013126 (1995)","journal-title":"Proc. Symposia Pure Math."},{"key":"9717_CR67","doi-asserted-by":"crossref","unstructured":"Martin-Dorel, \u00c9., Roux, P.: A reflexive tactic for polynomial positivity using numerical solvers and floating-point computations. In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, pp 90\u201399 (2017)","DOI":"10.1145\/3018610.3018622"},{"key":"9717_CR68","unstructured":"Mayero, M.: Formalisation et automatisation de preuves en analyses r\u00e9elle et num\u00e9rique. PhD thesis, Paris 6 (2001)"},{"key":"9717_CR69","doi-asserted-by":"publisher","first-page":"370","DOI":"10.1007\/978-3-642-39634-2_27","volume-title":"International Conference on Interactive Theorem Proving","author":"K Miyamoto","year":"2013","unstructured":"Miyamoto, K., Forsberg, F.N., Schwichtenberg, H.: Program extraction from nested definitions. In: International Conference on Interactive Theorem Proving, pp. 370\u2013385. Springer, Berlin (2013)"},{"key":"9717_CR70","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/978-3-642-22863-6_19","volume-title":"Interactive Theorem Proving","author":"D Monniaux","year":"2011","unstructured":"Monniaux, D., Corbineau, P.: On the generation of Positivstellensatz witnesses in degenerate cases. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) Interactive Theorem Proving, pp. 249\u2013264. Springer, Berlin Heidelberg (2011)"},{"key":"9717_CR71","doi-asserted-by":"crossref","unstructured":"Nakata, M.: A numerical evaluation of highly accurate multiple-precision arithmetic version of semidefinite programming solver: SDPA-GMP, -QD and -DD. In CACSD, pp 29\u201334 (2010)","DOI":"10.1109\/CACSD.2010.5612693"},{"key":"9717_CR72","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL\u2014A Proof Assistant for Higher-Order Logic, Volume 2283 of LNCS. Springer, Berlin (2002)","DOI":"10.1007\/3-540-45949-9"},{"issue":"1","key":"9717_CR73","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1017\/S0960129506005871","volume":"17","author":"R O\u2019Connor","year":"2007","unstructured":"O\u2019Connor, R.: A monadic, functional implementation of real numbers. Math. Struct. Comput. Sci. 17(1), 129\u2013159 (2007)","journal-title":"Math. Struct. Comput. Sci."},{"key":"9717_CR74","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/978-3-540-71067-7_21","volume-title":"International Conference on Theorem Proving in Higher Order Logics","author":"R O\u2019Connor","year":"2008","unstructured":"O\u2019Connor, R.: Certified exact transcendental real number computation in Coq. In: International Conference on Theorem Proving in Higher Order Logics, pp. 246\u2013261. Springer, Berlin (2008)"},{"key":"9717_CR75","unstructured":"Parrilo, P. A.: Structured Semidefinite Programs and Semialgebraic Geometry Methods in Robustness and Optimization. PhD thesis, California Inst.\u00a0Tech. (2000)"},{"issue":"2","key":"9717_CR76","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1016\/j.tcs.2008.09.025","volume":"409","author":"H Peyrl","year":"2008","unstructured":"Peyrl, H., Parrilo, P.A.: Computing sum of squares decompositions with rational coefficients. Theoret. Comput. Sci. 409(2), 269\u2013281 (2008)","journal-title":"Theoret. Comput. Sci."},{"key":"9717_CR77","doi-asserted-by":"crossref","unstructured":"Platzer, A.: Logics of dynamical systems. In Proceeding 2012 IEEE\/ACM Symposism. Logic Computer Science (LICS), pp 13\u201324. IEEE Computer Society (2012)","DOI":"10.1109\/LICS.2012.13"},{"issue":"4","key":"9717_CR78","doi-asserted-by":"publisher","first-page":"1831","DOI":"10.1016\/j.jfranklin.2014.01.002","volume":"351","author":"A Polyakov","year":"2014","unstructured":"Polyakov, A., Fridman, L.: Stability notions and lyapunov functions for sliding mode control systems. J. Franklin Inst. 351(4), 1831\u20131865 (2014)","journal-title":"J. Franklin Inst."},{"issue":"3","key":"9717_CR79","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":"9717_CR80","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1090\/conm\/253\/03936","volume":"253","author":"B Reznick","year":"2000","unstructured":"Reznick, B.: Some concrete aspects of Hilbert\u2019s 17th problem. Contemp. Math. 253, 251\u2013272 (2000)","journal-title":"Contemp. Math."},{"key":"9717_CR81","doi-asserted-by":"crossref","unstructured":"Rouhling, D.: A formal proof in Coq of a control function for the inverted pendulum. In Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp 28\u201341 (2018)","DOI":"10.1145\/3167101"},{"key":"9717_CR82","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1016\/B978-0-12-505630-4.50012-2","volume-title":"Reliability in Computing","author":"SM Rump","year":"1988","unstructured":"Rump, S.M.: Algorithms for verified inclusions: theory and practice. In: Reliability in Computing, pp. 109\u2013126. Elsevier, Amsterdam (1988)"},{"issue":"1","key":"9717_CR83","doi-asserted-by":"publisher","first-page":"171","DOI":"10.4064\/sm-2-1-171-180","volume":"2","author":"J Schauder","year":"1930","unstructured":"Schauder, J.: Fixed point in function spaces [der Fixpunktsatz in Funktionalra\u00fcmen (in German)]. Stud. Math. 2(1), 171\u2013180 (1930)","journal-title":"Stud. Math."},{"key":"9717_CR84","unstructured":"Schwichtenberg, H.: Constructive analysis with witnesses. Manuscript (2012)"},{"key":"9717_CR85","unstructured":"Schwichtenberg, H.: Constructive analysis with witnesses. Proof Technology and Computation. Natio Science Series, pp 323\u2013354 (2006)"},{"key":"9717_CR86","unstructured":"Schwichtenberg, H.: Minlog reference manual (2011)"},{"key":"9717_CR87","first-page":"490","volume-title":"Conference on Computability in Europe","author":"H Schwichtenberg","year":"2006","unstructured":"Schwichtenberg, H.: Inverting monotone continuous functions in constructive analysis. In: Conference on Computability in Europe, pp. 490\u2013504. Springer, Berlin (2006)"},{"issue":"3\u20134","key":"9717_CR88","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1007\/s00224-007-9027-4","volume":"43","author":"H Schwichtenberg","year":"2008","unstructured":"Schwichtenberg, H.: Realizability interpretation of proofs in constructive analysis. Theory of Computing Systems 43(3\u20134), 583\u2013602 (2008)","journal-title":"Theory of Computing Systems"},{"key":"9717_CR89","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/978-1-4020-8926-8_13","volume-title":"Logicism, Intuitionism, and Formalism","author":"H Schwichtenberg","year":"2009","unstructured":"Schwichtenberg, H.: Program extraction in constructive analysis. In: Logicism, Intuitionism, and Formalism, pp. 255\u2013275. Springer, Berlin (2009)"},{"key":"9717_CR90","doi-asserted-by":"publisher","first-page":"577","DOI":"10.1007\/BFb0012801","volume-title":"International Colloquium on Automata, Languages, and Programming","author":"DS Scott","year":"1982","unstructured":"Scott, D.S.: Domains for denotational semantics. In: International Colloquium on Automata, Languages, and Programming, pp. 577\u2013610. Springer, Berlin (1982)"},{"key":"9717_CR91","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139166386","volume-title":"Mathematical Theory of Domains","author":"V Stoltenberg-Hansen","year":"1994","unstructured":"Stoltenberg-Hansen, V., Lindstr\u00f6m, I., Griffor, E.R., et al.: Mathematical Theory of Domains, vol. 22. Cambridge University Press, Cambridge (1994)"},{"key":"9717_CR92","doi-asserted-by":"crossref","unstructured":"Streif, S., Rumschinski, P., Henrion, D., Findeisen, R.: Estimation of consistent parameter sets for continuous-time nonlinear systems using occupation measures and LMI relaxations. In 52nd IEEE Conference on Decision and Control, pp 6379\u20136384. IEEE (2013)","DOI":"10.1109\/CDC.2013.6760898"},{"key":"9717_CR93","doi-asserted-by":"crossref","unstructured":"Sturm, J.\u00a0F.: Using SeDuMi 1.02, a MATLAB toolbox for optimization over symmetric cones (1998)","DOI":"10.1080\/10556789908805766"},{"issue":"2","key":"9717_CR94","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1134\/S001226610802016X","volume":"44","author":"AV Surkov","year":"2008","unstructured":"Surkov, A.V.: On functional-differential equations with discontinuous right-hand side. Differ. Equ. 44(2), 278\u2013281 (2008)","journal-title":"Differ. Equ."},{"key":"9717_CR95","doi-asserted-by":"crossref","unstructured":"Tacchi, M., Cardozo, C., Henrion, D., Lasserre, J.: Approximating regions of attraction of a sparse polynomial differential system. arXiv preprint[SPACE]arXiv:1911.09500 (2019)","DOI":"10.1016\/j.ifacol.2020.12.1488"},{"key":"9717_CR96","unstructured":"The Coq Proof Assistant. http:\/\/coq.inria.fr\/"},{"key":"9717_CR97","unstructured":"The MOSEK optimization software. http:\/\/www.mosek.com\/"},{"issue":"2","key":"9717_CR98","doi-asserted-by":"publisher","first-page":"194","DOI":"10.2514\/1.G002754","volume":"40","author":"P Tsiotras","year":"2017","unstructured":"Tsiotras, P., Mesbahi, M.: Toward an algorithmic control theory. J. Guid. Control. Dyn. 40(2), 194\u2013196 (2017)","journal-title":"J. Guid. Control. Dyn."},{"issue":"1","key":"9717_CR99","first-page":"49","volume":"38","author":"L Vandenberghe","year":"1996","unstructured":"Vandenberghe, L., Boyd, S.: SIAM review. Semidefinite Program. 38(1), 49\u201395 (1996)","journal-title":"Semidefinite Program."},{"key":"9717_CR100","unstructured":"Wang, J., Magron, V., Lasserre, J.-B., Mai, N.\u00a0H.\u00a0A.: CS-TSSOS: Correlative and term sparsity for large-scale polynomial optimization. arXiv preprint[SPACE]arXiv:2005.02828 (2020)"},{"issue":"1","key":"9717_CR101","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1137\/20M1323564","volume":"31","author":"J Wang","year":"2021","unstructured":"Wang, J., Magron, V., Lasserre, J.-B.: Chordal-tssos: a moment-SOS hierarchy that exploits term sparsity with chordal extension. SIAM J. Optim. 31(1), 114\u2013141 (2021)","journal-title":"SIAM J. Optim."},{"issue":"1","key":"9717_CR102","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1137\/19M1307871","volume":"31","author":"J Wang","year":"2021","unstructured":"Wang, J., Magron, V., Lasserre, J.-B.: Tssos: a moment-SOS hierarchy that exploits term sparsity. SIAM J. Optim. 31(1), 30\u201358 (2021)","journal-title":"SIAM J. Optim."},{"key":"9717_CR103","volume-title":"Computable analysis: an introduction","author":"K Weihrauch","year":"2012","unstructured":"Weihrauch, K.: Computable analysis: an introduction. Springer, Berlin (2012)"},{"key":"9717_CR104","first-page":"175","volume-title":"Proofs Instead of Meaning Explanations: Understanding Classical vs Intuitionistic Mathematics from the Outside","author":"D Westerstahl","year":"2008","unstructured":"Westerstahl, D.: Proofs Instead of Meaning Explanations: Understanding Classical vs Intuitionistic Mathematics from the Outside, pp. 175\u2013194. Springer, Milan (2008)"},{"key":"9717_CR105","unstructured":"Yamashita, M., Fujisawa, K., Nakata, K., Nakata, M., Fukuda, M., Kobayashi, K., Goto, K.: A high-performance software package for semidefinite programs : SDPA7. Department of Information Sciences, Tokyo Institute of Technology, Tokyo, Japan, Technical report (2010)"},{"key":"9717_CR106","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-007-1347-5","volume-title":"Strict Finitism and the Logic of Mathematical Applications","author":"F Ye","year":"2011","unstructured":"Ye, F.: Strict Finitism and the Logic of Mathematical Applications, vol. 355. Springer, Berlin (2011)"},{"key":"9717_CR107","first-page":"262","volume-title":"Proceedings Working Conference Verified Software: Theories, Tools, and Experiments","author":"L Zou","year":"2013","unstructured":"Zou, L., Lv, J., Wang, S., Zhan, N., Tang, T., Yuan, L., Liu, Y.: Verifying Chinese train control system under a combined scenario by theorem proving. In: Proceedings Working Conference Verified Software: Theories, Tools, and Experiments, pp. 262\u2013280. Springer, Berlin (2013)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-024-09717-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-024-09717-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-024-09717-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,23]],"date-time":"2025-03-23T15:15:20Z","timestamp":1742742920000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-024-09717-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,25]]},"references-count":107,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2025,3]]}},"alternative-id":["9717"],"URL":"https:\/\/doi.org\/10.1007\/s10817-024-09717-2","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2025,1,25]]},"assertion":[{"value":"5 March 2023","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"20 December 2024","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"25 January 2025","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare no competing interests.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}}],"article-number":"2"}}