{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,3]],"date-time":"2026-03-03T04:09:04Z","timestamp":1772510944732,"version":"3.50.1"},"publisher-location":"Cham","reference-count":44,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031308192","type":"print"},{"value":"9783031308208","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,4,20]],"date-time":"2023-04-20T00:00:00Z","timestamp":1681948800000},"content-version":"vor","delay-in-days":109,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Numerical and symbolic methods for optimization are used extensively in engineering, industry, and finance. Various methods are used to reduce problems of interest to ones that are amenable to solution by these methods. We develop a framework for designing and applying such reductions, using the Lean programming language and interactive proof assistant. Formal verification makes the process more reliable, and the availability of an interactive framework and ambient mathematical library provides a robust environment for constructing the reductions and reasoning about them.\n<\/jats:p>","DOI":"10.1007\/978-3-031-30820-8_8","type":"book-chapter","created":{"date-parts":[[2023,4,19]],"date-time":"2023-04-19T19:02:36Z","timestamp":1681930956000},"page":"74-92","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Verified reductions for optimization"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7158-3595","authenticated-orcid":false,"given":"Alexander","family":"Bentkamp","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7242-5532","authenticated-orcid":false,"given":"Ramon Fern\u00e1ndez","family":"Mir","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1275-315X","authenticated-orcid":false,"given":"Jeremy","family":"Avigad","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,4,20]]},"reference":[{"key":"8_CR1","doi-asserted-by":"crossref","unstructured":"Agrawal, A., Verschueren, R., Diamond, S., Boyd, S.: A rewriting system for convex optimization problems. J. Control and Decision 5(1), 42\u201360 (2018)","DOI":"10.1080\/23307706.2017.1397554"},{"key":"8_CR2","doi-asserted-by":"publisher","unstructured":"Akbarpour, B., Abdel-Hamid, A.T., Tahar, S., Harrison, J.: Verifying a synthesized implementation of IEEE-754 floating-point exponential function using HOL. Comput. J. 53(4), 465\u2013488 (2010). https:\/\/doi.org\/10.1093\/comjnl\/bxp023","DOI":"10.1093\/comjnl\/bxp023"},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"Allamigeon, X., Katz, R.D.: A formalization of convex polyhedra based on the simplex method. J. Autom. Reason. 63(2), 323\u2013345 (2019)","DOI":"10.1007\/s10817-018-9477-1"},{"key":"8_CR4","doi-asserted-by":"publisher","unstructured":"Bachoc, C., Vallentin, F.: New upper bounds for kissing numbers from semidefinite programming. J. Amer. Math. Soc. 21(3), 909\u2013924 (2008). https:\/\/doi.org\/10.1090\/S0894-0347-07-00589-9","DOI":"10.1090\/S0894-0347-07-00589-9"},{"key":"8_CR5","unstructured":"Baudin, P., Cuoq, P., Filli\u00e2tre, J.C., March\u00e9, C., Monate, B., Moy, Y., Prevosto, V.: Acsl: ANSI \/ ISO c specification language (2020), https:\/\/frama-c.com\/html\/acsl.html, version 1.17"},{"key":"8_CR6","unstructured":"Bentkamp, A., Avigad, J.: Verified optimization (work in progress) (2022), Formal Mathematics for Mathematicians (FMM) workshop, 2021"},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"Bentkamp, A., Fern\u00e1ndez\u00a0Mir, R., Avigad, J.: Verified reductions for optimization (2023), https:\/\/arxiv.org\/abs\/2301.09347","DOI":"10.1007\/978-3-031-30820-8_8"},{"key":"8_CR8","doi-asserted-by":"crossref","unstructured":"Blanchette, J.C., Haslbeck, M.W., Matichuk, D., Nipkow, T.: Mining the archive of formal proofs. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.) Intelligent Computer Mathematics (CICM) 2015. pp. 3\u201317. Springer (2015)","DOI":"10.1007\/978-3-319-20615-8_1"},{"key":"8_CR9","doi-asserted-by":"publisher","unstructured":"Boldo, S., Filli\u00e2tre, J.: Formal verification of floating-point programs. In: 18th IEEE Symposium on Computer Arithmetic (ARITH-18) 2007, 25-27 June 2007, Montpellier, France. pp. 187\u2013194. IEEE Computer Society (2007). https:\/\/doi.org\/10.1109\/ARITH.2007.20","DOI":"10.1109\/ARITH.2007.20"},{"key":"8_CR10","unstructured":"Boyd, S.P., Vandenberghe, L.: Convex Optimization. Cambridge University Press (2014), https:\/\/web.stanford.edu\/~boyd\/cvxbook\/"},{"key":"8_CR11","doi-asserted-by":"crossref","unstructured":"Cohen, R., Davy, G., Feron, E., Garoche, P.L.: Formal verification for embedded implementation of convex optimization algorithms. IFAC-PapersOnLine 50(1), 5867\u20135874 (2017), 20th IFAC World Congress","DOI":"10.1016\/j.ifacol.2017.08.1300"},{"key":"8_CR12","doi-asserted-by":"crossref","unstructured":"Cohen, R., Feron, E., Garoche, P.: Verification and validation of convex optimization algorithms for model predictive control. Journal of Aerospace Information Systems 17(5), 257\u2013270 (2020)","DOI":"10.2514\/1.I010686"},{"key":"8_CR13","unstructured":"Cordwell, K., Tan, Y.K., Platzer, A.: A verified decision procedure for univariate real arithmetic with the BKR algorithm. In: Cohen, L., Kaliszyk, C. (eds.) Interactive Theorem Proving (ITP) 2021. LIPIcs, vol.\u00a0193, pp. 14:1\u201314:20. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2021)"},{"key":"8_CR14","doi-asserted-by":"crossref","unstructured":"Deshmukh, J.V., Sankaranarayanan, S.: Formal techniques for verification and testing of cyber-physical systems. In: Al\u00a0Faruque, M.A., Canedo, A. (eds.) Design Automation of Cyber-Physical Systems. pp. 69\u2013105. Springer, Cham (2019)","DOI":"10.1007\/978-3-030-13050-3_4"},{"key":"8_CR15","unstructured":"Diamond, S., Boyd, S.: CVXPY: A Python-embedded modeling language for convex optimization. J. Machine Learning Research 17(83), \u00a01\u20135 (2016)"},{"key":"8_CR16","doi-asserted-by":"publisher","unstructured":"Fr\u00e4nzle, M., Herde, C., Teige, T., Ratschan, S., Schubert, T.: Efficient solving of large non-linear arithmetic constraint systems with complex Boolean structure. J. Satisf. Boolean Model. Comput. 1(3-4), 209\u2013236 (2007). https:\/\/doi.org\/10.3233\/sat190012","DOI":"10.3233\/sat190012"},{"key":"8_CR17","doi-asserted-by":"crossref","unstructured":"Fu, A., Narasimhan, B., Boyd, S.: CVXR: An R package for disciplined convex optimization. Journal of Statistical Software 94(14), 1\u201334 (2020)","DOI":"10.18637\/jss.v094.i14"},{"key":"8_CR18","doi-asserted-by":"crossref","unstructured":"Gao, S., Avigad, J., Clarke, E.M.: $$\\delta $$-complete decision procedures for satisfiability over the reals. In: Gramlich, B., Miller, D., Sattler, U. (eds.) Automated Reasoning (IJCAR) 2012. pp. 286\u2013300. Springer (2012)","DOI":"10.1007\/978-3-642-31365-3_23"},{"key":"8_CR19","doi-asserted-by":"publisher","unstructured":"Goodloe, A., Mu\u00f1oz, C.A., Kirchner, F., Correnson, L.: Verification of numerical programs: From real numbers to floating point numbers. In: Brat, G., Rungta, N., Venet, A. (eds.) NASA Formal Methods (NFM) 2013. pp. 441\u2013446. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-38088-4_31","DOI":"10.1007\/978-3-642-38088-4_31"},{"key":"8_CR20","unstructured":"Grant, M., Boyd, S.: CVX: Matlab software for disciplined convex programming, version 2.1. http:\/\/cvxr.com\/cvx (Mar 2014)"},{"key":"8_CR21","doi-asserted-by":"crossref","unstructured":"Grant, M., Boyd, S., Ye, Y.: Disciplined convex programming. In: Global optimization, pp. 155\u2013210. Springer (2006)","DOI":"10.1007\/0-387-30528-9_7"},{"key":"8_CR22","unstructured":"Grechuk, B.: Lower semicontinuous functions. Archive of Formal Proofs (Jan 2011), https:\/\/isa-afp.org\/entries\/Lower_Semicontinuous.html, Formal proof development"},{"key":"8_CR23","unstructured":"Gurobi Optimization, LLC: Gurobi Optimizer Reference Manual (2022), https:\/\/www.gurobi.com"},{"key":"8_CR24","doi-asserted-by":"crossref","unstructured":"Harrison, J.: Verifying nonlinear real formulas via sums of squares. In: Schneider, K., Brandt, J. (eds.) Theorem Proving in Higher Order Logics (TPHOLs) 2007. pp. 102\u2013118. Springer (2007)","DOI":"10.1007\/978-3-540-74591-4_9"},{"key":"8_CR25","doi-asserted-by":"crossref","unstructured":"Kong, S., Solar-Lezama, A., Gao, S.: Delta-decision procedures for exists-forall problems over the reals. In: Chockler, H., Weissenbacher, G. (eds.) Computer Aided Verification (CAV) 2018, Part II. pp. 219\u2013235. Springer (2018)","DOI":"10.1007\/978-3-319-96142-2_15"},{"key":"8_CR26","unstructured":"L\u00f6fberg, J.: Yalmip : A toolbox for modeling and optimization in matlab. In: Computer Aided Control System Design (CACSD) 2004. pp. 284\u2013289 (2004)"},{"key":"8_CR27","doi-asserted-by":"publisher","unstructured":"Magron, V., Allamigeon, X., Gaubert, S., Werner, B.: Formal proofs for nonlinear optimization. J. Formaliz. Reason. 8(1), 1\u201324 (2015). https:\/\/doi.org\/10.6092\/issn.1972-5787\/4319","DOI":"10.6092\/issn.1972-5787\/4319"},{"key":"8_CR28","doi-asserted-by":"publisher","unstructured":"Martin-Dorel, \u00c9., Roux, P.: A reflexive tactic for polynomial positivity using numerical solvers and floating-point computations. In: Bertot, Y., Vafeiadis, V. (eds.) Certified Programs and Proofs (CPP) 2017. pp. 90\u201399. ACM (2017). https:\/\/doi.org\/10.1145\/3018610.3018622","DOI":"10.1145\/3018610.3018622"},{"key":"8_CR29","unstructured":"Mathlib Community: The Lean mathematical library. In: Blanchette, J., Hritcu, C. (eds.) Certified Programs and Proofs (CPP) 2020. pp. 367\u2013381. ACM (2020)"},{"key":"8_CR30","unstructured":"MOSEK ApS: Introducing the MOSEK Optimization Suite (2022), https:\/\/docs.mosek.com\/latest\/intro"},{"key":"8_CR31","unstructured":"MOSEK ApS: MOSEK Modeling Cookbook (2022), https:\/\/docs.mosek.com\/modeling-cookbook"},{"key":"8_CR32","doi-asserted-by":"publisher","unstructured":"de\u00a0Moura, L., Ullrich, S.: The Lean 4 theorem prover and programming language. In: Platzer, A., Sutcliffe, G. (eds.) Automated Deduction (CADE) 2021. pp. 625\u2013635. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-79876-5_37","DOI":"10.1007\/978-3-030-79876-5_37"},{"key":"8_CR33","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L.M., Kong, S., Avigad, J., van Doorn, F., von Raumer, J.: The Lean theorem prover (system description). In: Felty, A.P., Middeldorp, A. (eds.) Conference on Automated Deduction (CADE) 2015. pp. 378\u2013388. Springer (2015)","DOI":"10.1007\/978-3-319-21401-6_26"},{"key":"8_CR34","doi-asserted-by":"publisher","unstructured":"Mu\u00f1oz, C.A., Narkawicz, A.J., Dutle, A.: A decision procedure for univariate polynomial systems based on root counting and interval subdivision. J. Formaliz. Reason. 11(1), 19\u201341 (2018). https:\/\/doi.org\/10.6092\/issn.1972-5787\/8212","DOI":"10.6092\/issn.1972-5787\/8212"},{"key":"8_CR35","doi-asserted-by":"crossref","unstructured":"Narkawicz, A., Mu\u00f1oz, C.A.: A formally verified generic branching algorithm for global optimization. In: Cohen, E., Rybalchenko, A. (eds.) Verified Software: Theories, Tools, Experiments (VSTTE) 2013. pp. 326\u2013343. Springer (2013)","DOI":"10.1007\/978-3-642-54108-7_17"},{"key":"8_CR36","doi-asserted-by":"publisher","unstructured":"Nesterov, Y.: Lectures on convex optimization. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-91578-4,second edition","DOI":"10.1007\/978-3-319-91578-4"},{"key":"8_CR37","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL - A Proof Assistant for Higher-Order Logic. Springer (2002)","DOI":"10.1007\/3-540-45949-9"},{"key":"8_CR38","doi-asserted-by":"publisher","unstructured":"Ratschan, S., She, Z.: Safety verification of hybrid systems by constraint propagation-based abstraction refinement. ACM Trans. Embed. Comput. Syst. 6(1), \u00a08 (2007). https:\/\/doi.org\/10.1145\/1210268.1210276","DOI":"10.1145\/1210268.1210276"},{"key":"8_CR39","unstructured":"Rockafellar, R.T.: Convex analysis. Princeton University Press, Princeton, N.J. (1970)"},{"key":"8_CR40","doi-asserted-by":"crossref","unstructured":"Solovyev, A., Hales, T.C.: Formal verification of nonlinear inequalities with Taylor interval approximations. In: Brat, G., Rungta, N., Venet, A. (eds.) NASA Formal Methods (NFM) 2013. pp. 383\u2013397. Springer (2013)","DOI":"10.1007\/978-3-642-38088-4_26"},{"key":"8_CR41","doi-asserted-by":"crossref","unstructured":"Sturm, J.F.: Using Sedumi 1.02, a Matlab toolbox for optimization over symmetric cones. Optimization methods and software 11(1-4), 625\u2013653 (1999)","DOI":"10.1080\/10556789908805766"},{"key":"8_CR42","doi-asserted-by":"crossref","unstructured":"Udell, M., Mohan, K., Zeng, D., Hong, J., Diamond, S., Boyd, S.: Convex optimization in Julia. SC14 Workshop on High Performance Technical Computing in Dynamic Languages (2014)","DOI":"10.1109\/HPTCDL.2014.5"},{"key":"8_CR43","doi-asserted-by":"crossref","unstructured":"Vishnoi, N.: Algorithms for Convex Optimization. Cambridge University Press (2021)","DOI":"10.1017\/9781108699211"},{"key":"8_CR44","unstructured":"Yu, L.: A formal model of IEEE floating point arithmetic. Archive of Formal Proofs (July 2013), https:\/\/www.isa-afp.org\/entries\/IEEE_Floating_Point.shtml"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-30820-8_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,2]],"date-time":"2023-08-02T11:03:45Z","timestamp":1690974225000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-30820-8_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031308192","9783031308208"],"references-count":44,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-30820-8_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"20 April 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 April 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 April 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2023\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"169","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"56","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"6","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"33% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}