{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,28]],"date-time":"2025-05-28T06:40:04Z","timestamp":1748414404424,"version":"3.41.0"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031669965"},{"type":"electronic","value":"9783031669972"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"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":[[2024]]},"DOI":"10.1007\/978-3-031-66997-2_11","type":"book-chapter","created":{"date-parts":[[2024,8,3]],"date-time":"2024-08-03T20:03:12Z","timestamp":1722715392000},"page":"183-202","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Transforming Optimization Problems into\u00a0Disciplined Convex Programming Form"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7242-5532","authenticated-orcid":false,"given":"Ramon","family":"Fern\u00e1ndez Mir","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3863-8336","authenticated-orcid":false,"given":"Paul B.","family":"Jackson","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0007-6410-3681","authenticated-orcid":false,"given":"Siddharth","family":"Bhat","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0409-1363","authenticated-orcid":false,"given":"Andr\u00e9s","family":"Goens","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3874-6003","authenticated-orcid":false,"given":"Tobias","family":"Grosser","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,7,29]]},"reference":[{"key":"11_CR1","doi-asserted-by":"publisher","first-page":"1643","DOI":"10.1007\/s11590-020-01561-8","volume":"14","author":"A Agrawal","year":"2020","unstructured":"Agrawal, A., Boyd, S.: Disciplined quasiconvex programming. Optim. Lett. 14, 1643\u20131657 (2020). https:\/\/doi.org\/10.1007\/s11590-020-01561-8","journal-title":"Optim. Lett."},{"key":"11_CR2","doi-asserted-by":"publisher","first-page":"961","DOI":"10.1007\/s11590-019-01422-z","volume":"13","author":"A Agrawal","year":"2019","unstructured":"Agrawal, A., Diamond, S., Boyd, S.: Disciplined geometric programming. Optim. Lett. 13, 961\u2013976 (2019). https:\/\/doi.org\/10.1007\/s11590-019-01422-z","journal-title":"Optim. Lett."},{"key":"11_CR3","doi-asserted-by":"publisher","unstructured":"Andersen, E.D., Andersen, K.D.: The MOSEK interior point optimizer for linear programming: an implementation of the homogeneous algorithm. In: Frenk, H., Roos, K., Terlaky, T., Zhang, S. (eds.) High Performance Optimization, pp. 197\u2013232. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/978-1-4757-3216-0_8","DOI":"10.1007\/978-1-4757-3216-0_8"},{"key":"11_CR4","doi-asserted-by":"publisher","unstructured":"Bentkamp, A., Fern\u00e1ndez\u00a0Mir, R., Avigad, J.: Verified reductions for optimization. In: Sankaranarayanan, S., Sharygina, N. (eds.) International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 74\u201392. Springer, Heidelberg (2023). https:\/\/doi.org\/10.1007\/978-3-031-30820-8_8","DOI":"10.1007\/978-3-031-30820-8_8"},{"key":"11_CR5","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511804441","volume-title":"Convex Optimization","author":"SP Boyd","year":"2004","unstructured":"Boyd, S.P., Vandenberghe, L.: Convex Optimization. Cambridge University Press, Cambridge (2004). https:\/\/doi.org\/10.1017\/CBO9780511804441"},{"key":"11_CR6","doi-asserted-by":"publisher","unstructured":"Mathlib Community, T.: The Lean mathematical library. In: CPP 2020, pp. 367\u2013381. Association for Computing Machinery, New York (2020). https:\/\/doi.org\/10.1145\/3372885.3373824","DOI":"10.1145\/3372885.3373824"},{"key":"11_CR7","doi-asserted-by":"publisher","unstructured":"De\u00a0Moura, L., Bj\u00f8rner, N.: Efficient e-matching for SMT solvers. In: Pfenning, F. (ed.) Automated Deduction\u2013CADE-21: 21st International Conference on Automated Deduction, Bremen, Germany, 17\u201320 July 2007, Proceedings 21, pp. 183\u2013198. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73595-3_13","DOI":"10.1007\/978-3-540-73595-3_13"},{"key":"11_CR8","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"},{"issue":"3","key":"11_CR9","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1145\/1066100.1066102","volume":"52","author":"D Detlefs","year":"2005","unstructured":"Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM (JACM) 52(3), 365\u2013473 (2005). https:\/\/doi.org\/10.1145\/1066100.1066102","journal-title":"J. ACM (JACM)"},{"issue":"83","key":"11_CR10","first-page":"1","volume":"17","author":"S Diamond","year":"2016","unstructured":"Diamond, S., Boyd, S.: CVXPY: a python-embedded modeling language for convex optimization. J. Mach. Learn. Res. 17(83), 1\u20135 (2016)","journal-title":"J. Mach. Learn. Res."},{"key":"11_CR11","doi-asserted-by":"publisher","unstructured":"Domahidi, A., Chu, E., Boyd, S.: ECOS: an SOCP solver for embedded systems. In: 2013 European Control Conference (ECC), pp. 3071\u20133076. IEEE (2013). https:\/\/doi.org\/10.23919\/ECC.2013.6669541","DOI":"10.23919\/ECC.2013.6669541"},{"key":"11_CR12","doi-asserted-by":"publisher","unstructured":"Flatt, O., Coward, S., Willsey, M., Tatlock, Z., Panchekha, P.: Small proofs from congruence closure. In: 2022 Formal Methods in Computer-Aided Design (FMCAD), pp. 75\u201383. IEEE (2022). https:\/\/doi.org\/10.34727\/2022\/isbn.978-3-85448-053-2_13","DOI":"10.34727\/2022\/isbn.978-3-85448-053-2_13"},{"key":"11_CR13","doi-asserted-by":"publisher","unstructured":"Fu, A., Narasimhan, B., Boyd, S.: CVXR: an R package for disciplined convex optimization. J. Stat. Softw. 94, 1\u201334 (2020). https:\/\/doi.org\/10.18637\/jss.v094.i14","DOI":"10.18637\/jss.v094.i14"},{"key":"11_CR14","unstructured":"Gj\u00f8rup, E.H., Spitters, B.: Congruence closure in cubical type theory. In: Workshop on Homotopy Type Theory\/Univalent Foundations (2020). https:\/\/www.cs.au.dk\/~spitters\/Emil.pdf"},{"key":"11_CR15","unstructured":"Grant, M., Boyd, S.: CVX: MATLAB software for disciplined convex programming, version 2.1 (2014). http:\/\/cvxr.com\/cvx"},{"key":"11_CR16","doi-asserted-by":"publisher","unstructured":"Grant, M., Boyd, S., Ye, Y.: Disciplined convex programming. In: Global Optimization: From Theory to Implementation, pp. 155\u2013210 (2006). https:\/\/doi.org\/10.1007\/0-387-30528-9_7","DOI":"10.1007\/0-387-30528-9_7"},{"key":"11_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/978-3-540-74591-4_9","volume-title":"Theorem Proving in Higher Order Logics","author":"J Harrison","year":"2007","unstructured":"Harrison, J.: Verifying nonlinear real formulas via sums of squares. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol. 4732, pp. 102\u2013118. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-74591-4_9"},{"key":"11_CR18","unstructured":"H\u00e4rter, V., Jansson, C., Lange, M.: VSDP: A MATLAB toolbox for verified semidefinite-quadratic-linear programming. Optimization Online (2012). https:\/\/optimization-online.org\/?p=12271"},{"issue":"5","key":"11_CR19","doi-asserted-by":"publisher","first-page":"1038","DOI":"10.1145\/502102.502106","volume":"48","author":"TJ Hickey","year":"2001","unstructured":"Hickey, T.J., Ju, Q., van Emden, M.H.: Interval arithmetic: from principles to implementation. J. ACM 48(5), 1038\u20131068 (2001). https:\/\/doi.org\/10.1145\/502102.502106","journal-title":"J. ACM"},{"key":"11_CR20","doi-asserted-by":"publisher","unstructured":"Limperg, J., From, A.H.: Aesop: white-box best-first proof search for Lean. In: Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 253\u2013266 (2023). https:\/\/doi.org\/10.1145\/3573105.3575671","DOI":"10.1145\/3573105.3575671"},{"key":"11_CR21","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":"11_CR22","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"625","DOI":"10.1007\/978-3-030-79876-5_37","volume-title":"Automated Deduction \u2013 CADE 28","author":"L Moura","year":"2021","unstructured":"Moura, L., Ullrich, S.: The lean 4 theorem prover and programming language. In: Platzer, A., Sutcliffe, G. (eds.) CADE 2021. LNCS (LNAI), vol. 12699, pp. 625\u2013635. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-79876-5_37"},{"issue":"2","key":"11_CR23","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1145\/322186.322198","volume":"27","author":"G Nelson","year":"1980","unstructured":"Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. J. ACM (JACM) 27(2), 356\u2013364 (1980). https:\/\/doi.org\/10.1145\/322186.322198","journal-title":"J. ACM (JACM)"},{"key":"11_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1007\/978-3-540-32033-3_33","volume-title":"Term Rewriting and Applications","author":"R Nieuwenhuis","year":"2005","unstructured":"Nieuwenhuis, R., Oliveras, A.: Proof-producing congruence closure. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 453\u2013468. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-32033-3_33"},{"issue":"6","key":"11_CR25","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2813885.2737959","volume":"50","author":"P Panchekha","year":"2015","unstructured":"Panchekha, P., Sanchez-Stern, A., Wilcox, J.R., Tatlock, Z.: Automatically improving accuracy for floating point expressions. ACM SIGPLAN Not. 50(6), 1\u201311 (2015). https:\/\/doi.org\/10.1145\/2813885.2737959","journal-title":"ACM SIGPLAN Not."},{"issue":"2","key":"11_CR26","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1016\/0167-6423(83)90008-4","volume":"3","author":"LC Paulson","year":"1983","unstructured":"Paulson, L.C.: A higher-order implementation of rewriting. Sci. Comput. Program. 3(2), 119\u2013149 (1983). https:\/\/doi.org\/10.1016\/0167-6423(83)90008-4","journal-title":"Sci. Comput. Program."},{"key":"11_CR27","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-319-40229-1_8","volume-title":"Automated Reasoning","author":"D Selsam","year":"2016","unstructured":"Selsam, D., de Moura, L.: Congruence closure in intensional type theory. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 99\u2013115. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40229-1_8"},{"issue":"2","key":"11_CR28","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1145\/321879.321884","volume":"22","author":"RE Tarjan","year":"1975","unstructured":"Tarjan, R.E.: Efficiency of a good but not linear set union algorithm. J. ACM (JACM) 22(2), 215\u2013225 (1975). https:\/\/doi.org\/10.1145\/321879.321884","journal-title":"J. ACM (JACM)"},{"key":"11_CR29","doi-asserted-by":"publisher","unstructured":"Tate, R., Stepp, M., Tatlock, Z., Lerner, S.: Equality saturation: a new approach to optimization. In: Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 264\u2013276 (2009). https:\/\/doi.org\/10.1145\/1480881.1480915","DOI":"10.1145\/1480881.1480915"},{"key":"11_CR30","doi-asserted-by":"publisher","unstructured":"Udell, M., Mohan, K., Zeng, D., Hong, J., Diamond, S., Boyd, S.: Convex optimization in Julia. In: 2014 First Workshop for High Performance Technical Computing in Dynamic Languages, pp. 18\u201328. IEEE (2014). https:\/\/doi.org\/10.1109\/HPTCDL.2014.5","DOI":"10.1109\/HPTCDL.2014.5"},{"key":"11_CR31","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-030-51054-1_10","volume-title":"Automated Reasoning","author":"S Ullrich","year":"2020","unstructured":"Ullrich, S., de Moura, L.: Beyond notations: hygienic macro expansion for theorem proving languages. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) IJCAR 2020. LNCS (LNAI), vol. 12167, pp. 167\u2013182. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-51054-1_10"},{"key":"11_CR32","doi-asserted-by":"publisher","unstructured":"VanHattum, A., Nigam, R., Lee, V.T., Bornholt, J., Sampson, A.: Vectorization for digital signal processors via equality saturation. In: Proceedings of the 26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, pp. 874\u2013886 (2021). https:\/\/doi.org\/10.1145\/3445814.3446707","DOI":"10.1145\/3445814.3446707"},{"key":"11_CR33","doi-asserted-by":"publisher","unstructured":"Wang, Y.R., Hutchison, S., Suciu, D., Howe, B., Leang, J.: SPORES: sum-product optimization via relational equality saturation for large scale linear algebra. Proc. VLDB Endow. 13(11), 1919\u20131932 (2020). https:\/\/doi.org\/10.14778\/3407790.3407799. http:\/\/www.vldb.org\/pvldb\/vol13\/p1919-wang.pdf","DOI":"10.14778\/3407790.3407799"},{"key":"11_CR34","doi-asserted-by":"publisher","unstructured":"Willsey, M., Nandi, C., Wang, Y.R., Flatt, O., Tatlock, Z., Panchekha, P.: Egg: fast and extensible equality saturation. Proc. ACM Program. Lang. 5(POPL), 1\u201329 (2021). https:\/\/doi.org\/10.1145\/3434304","DOI":"10.1145\/3434304"},{"issue":"1","key":"11_CR35","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1090\/S0273-0979-04-01040-7","volume":"42","author":"M Wright","year":"2005","unstructured":"Wright, M.: The interior-point revolution in optimization: history, recent developments, and lasting consequences. Bull. Am. Math. Soc. 42(1), 39\u201356 (2005). https:\/\/doi.org\/10.1090\/S0273-0979-04-01040-7","journal-title":"Bull. Am. Math. Soc."},{"key":"11_CR36","doi-asserted-by":"publisher","unstructured":"Yamashita, M., Fujisawa, K., Kojima, M.: Implementation and evaluation of SDPA 6.0 (semidefinite programming algorithm 6.0). Optim. Methods Softw. 18(4), 491\u2013505 (2003). https:\/\/doi.org\/10.1080\/1055678031000118482","DOI":"10.1080\/1055678031000118482"},{"key":"11_CR37","unstructured":"Yang, Y., Phothilimthana, P., Wang, Y., Willsey, M., Roy, S., Pienaar, J.: Equality saturation for tensor graph superoptimization. Proc. Mach. Learn. Syst. 3, 255\u2013268 (2021). https:\/\/proceedings.mlsys.org\/paper_files\/paper\/2021\/file\/cc427d934a7f6c0663e5923f49eba531-Paper.pdf"},{"key":"11_CR38","doi-asserted-by":"publisher","unstructured":"Zhang, Y., et al.: Better together: unifying datalog and equality saturation. Proc. ACM Program. Lang. 7(PLDI), 468\u2013492 (2023). https:\/\/doi.org\/10.1145\/3591239","DOI":"10.1145\/3591239"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-66997-2_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,28]],"date-time":"2025-05-28T06:05:28Z","timestamp":1748412328000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-66997-2_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031669965","9783031669972"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-66997-2_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"29 July 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CICM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Intelligent Computer Mathematics","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Montreal, QC","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","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":"5 August 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 August 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"mkm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/cicm-conference.org\/2024\/cicm.php","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}