{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,28]],"date-time":"2026-04-28T03:43:52Z","timestamp":1777347832960,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":39,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662491218","type":"print"},{"value":"9783662491225","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,12,25]],"date-time":"2015-12-25T00:00:00Z","timestamp":1451001600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-662-49122-5_8","type":"book-chapter","created":{"date-parts":[[2015,12,24]],"date-time":"2015-12-24T05:01:36Z","timestamp":1450933296000},"page":"166-184","source":"Crossref","is-referenced-by-count":19,"title":["Polyhedral Approximation of Multivariate Polynomials Using Handelman\u2019s Theorem"],"prefix":"10.1007","author":[{"given":"Alexandre","family":"Mar\u00e9chal","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexis","family":"Fouilh\u00e9","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tim","family":"King","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Monniaux","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"P\u00e9rin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,12,25]]},"reference":[{"issue":"1\u20132","key":"8_CR1","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.scico.2007.08.001","volume":"72","author":"R Bagnara","year":"2008","unstructured":"Bagnara, R., Hill, P.M., Zaffanella, E.: The Parma Polyhedra Library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Sci. Comput. Program. 72(1\u20132), 3\u201321 (2008). Tool available at \n                      www.cs.unipr.it\/ppl\/","journal-title":"Sci. Comput. Program."},{"key":"8_CR2","unstructured":"Barrett, C., Stump, A., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2010). \n                      http:\/\/www.SMT-LIB.org"},{"issue":"11","key":"8_CR3","doi-asserted-by":"publisher","first-page":"1691","DOI":"10.1109\/TCAD.2011.2161307","volume":"30","author":"D Boland","year":"2011","unstructured":"Boland, D., Constantinides, G.A.: Bounding variable values and round-off effects using Handelman representations. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 30(11), 1691\u20131704 (2011)","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"key":"8_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"100","DOI":"10.1007\/978-3-319-22102-1_7","volume-title":"Interactive Theorem Proving","author":"S Boulm\u00e9","year":"2015","unstructured":"Boulm\u00e9, S., Mar\u00e9chal, A.: Refinement to certify abstract interpretations, illustrated on linearization for polyhedra. In: Urban, C., Zhang, X. (eds.) Interactive Theorem Proving. LNCS, vol. 9236, pp. 100\u2013116. Springer, Heidelberg (2015)"},{"key":"8_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1007\/978-3-642-03237-0_21","volume-title":"Static Analysis","author":"L Chen","year":"2009","unstructured":"Chen, L., Min\u00e9, A., Wang, J., Cousot, P.: Interval polyhedra: an abstract domain to infer interval linear relationships. In: Palsberg, J., Su, Z. (eds.) SAS 2009. LNCS, vol. 5673, pp. 309\u2013325. Springer, Heidelberg (2009)"},{"key":"8_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/978-3-642-15582-6_5","volume-title":"Mathematical Software \u2013 ICMS 2010","author":"S Chevillard","year":"2010","unstructured":"Chevillard, S., Jolde\u015f, M., Lauter, C.: Sollya: an environment for the development of numerical codes. In: Fukuda, K., Hoeven, J., Joswig, M., Takayama, N. (eds.) ICMS 2010. LNCS, vol. 6327, pp. 28\u201331. Springer, Heidelberg (2010)"},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"Chevillard, S., Jolde\u015f, M., Lauter, C.: Certified and fast computation of supremum norms of approximation errors. In: Computer Arithmetic (ARITH), pp. 169\u2013176. IEEE Computer Society, June 2009","DOI":"10.1109\/ARITH.2009.18"},{"key":"8_CR8","unstructured":"Chvatal, V.: Linear Programming. Series of books in the Mathematical Sciences. W. H., Freeman (1983)"},{"issue":"8","key":"8_CR9","doi-asserted-by":"publisher","first-page":"983","DOI":"10.1109\/TVLSI.2008.2002049","volume":"17","author":"P Clauss","year":"2009","unstructured":"Clauss, P., Fernandez, F.J., Gabervetsky, D., Verdoolaege, S.: Symbolic polynomial maximization over convex sets and its application to memory requirement estimation. IEEE Trans. Very Large Scale Integr. (VLSI) Syst. 17(8), 983\u2013996 (2009)","journal-title":"IEEE Trans. Very Large Scale Integr. (VLSI) Syst."},{"key":"8_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"442","DOI":"10.1007\/978-3-642-31612-8_35","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"F Corzilius","year":"2012","unstructured":"Corzilius, F., Loup, U., Junges, S., \u00c1brah\u00e1m, E.: SMT-RAT: an SMT-compliant nonlinear real arithmetic toolbox. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 442\u2013448. Springer, Heidelberg (2012)"},{"key":"8_CR11","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: ACM Principles of Programming Languages (POPL), pp.84\u201397. ACM Press, January 1978","DOI":"10.1145\/512760.512770"},{"key":"8_CR12","unstructured":"Dantzig, G.B., Thapa, M.N.: Linear Programming 2: Theory and Extensions. Springer, Operations Research (2003)"},{"key":"8_CR13","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 Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"8_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-35873-9_1","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"L Moura de","year":"2013","unstructured":"de Moura, L., Jovanovi\u0107, D.: A model-constructing satisfiability calculus. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 1\u201312. Springer, Heidelberg (2013)"},{"key":"8_CR15","unstructured":"Deters, M., Reynolds, A., King, T., Barrett, C., Tinelli, C.: A tour of cvc4: How it works, and how to use it. In: Proceedings of the 14th Conference on Formal Methods in Computer-Aided Design, FMCAD 2014, pp. 4:7\u20134:7, Austin, TX, 2014. FMCAD Inc"},{"key":"8_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"737","DOI":"10.1007\/978-3-319-08867-9_49","volume-title":"Computer Aided Verification","author":"B Dutertre","year":"2014","unstructured":"Dutertre, B.: Yices\u00a02.2. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 737\u2013744. Springer, Heidelberg (2014)"},{"key":"8_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/11817963_11","volume-title":"Computer Aided Verification","author":"B Dutertre","year":"2006","unstructured":"Dutertre, B., de Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 81\u201394. Springer, Heidelberg (2006)"},{"key":"8_CR18","unstructured":"Dutertre, B., De Moura, L.: Integrating simplex with DPLL(T). Technical Report SRI-CSL-06-01, SRI International, computer science laboratory (2006)"},{"issue":"3","key":"8_CR19","doi-asserted-by":"crossref","first-page":"243","DOI":"10.1051\/ro\/1988220302431","volume":"22","author":"P Feautrier","year":"1988","unstructured":"Feautrier, P.: Parametric integer programming. RAIRO Rech. Op\u00e9rationnelle 22(3), 243\u2013268 (1988)","journal-title":"RAIRO Rech. Op\u00e9rationnelle"},{"key":"8_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1007\/978-3-642-38856-9_19","volume-title":"Static Analysis","author":"A Fouilhe","year":"2013","unstructured":"Fouilhe, A., Monniaux, D., P\u00e9rin, M.: Efficient generation of correctness certificates for the abstract domain of polyhedra. In: Logozzo, F., F\u00e4hndrich, M. (eds.) Static Analysis. LNCS, vol. 7935, pp. 345\u2013365. Springer, Heidelberg (2013)"},{"key":"8_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/978-3-540-27813-9_14","volume-title":"Computer Aided Verification","author":"H Ganzinger","year":"2004","unstructured":"Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): fast decision procedures. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 175\u2013188. Springer, Heidelberg (2004)"},{"key":"8_CR22","unstructured":"Halbwachs, N.: D\u00e9termination automatique de relations lin\u00e9aires v\u00e9rifi\u00e9es par les variables d\u2019un programme. Universit\u00e9 de Grenoble, Th\u00e8se de doctorat de troisi\u00e8me cycle, March 1979"},{"issue":"1","key":"8_CR23","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":"8_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"661","DOI":"10.1007\/978-3-642-02658-4_52","volume-title":"Computer Aided Verification","author":"B Jeannet","year":"2009","unstructured":"Jeannet, B., Min\u00e9, A.: Apron: a library of numerical abstract domains for static analysis. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 661\u2013667. Springer, Heidelberg (2009)"},{"key":"8_CR25","doi-asserted-by":"crossref","unstructured":"Jones, C.N., Kerrigan, E.C., Maciejowski, J.M.: Lexicographic perturbation for multiparametric linear programming with applications to control. Automatica (2007)","DOI":"10.1016\/j.automatica.2007.03.008"},{"key":"8_CR26","doi-asserted-by":"crossref","unstructured":"Jourdan, J.-H., Laporte, V., Blazy, S., Leroy, X., Pichardie, D.: A formally-verified C static analyzer. In: ACM Principles of Programming Languages (POPL), pp. 247\u2013259. ACM Press, January 2015","DOI":"10.1145\/2775051.2676966"},{"key":"8_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1007\/978-3-642-31365-3_27","volume-title":"Automated Reasoning","author":"D Jovanovi\u0107","year":"2012","unstructured":"Jovanovi\u0107, D., de Moura, L.: Solving non-linear arithmetic. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 339\u2013354. Springer, Heidelberg (2012)"},{"key":"8_CR28","unstructured":"Khanh, T.V., Vu, X., Ogawa, M.: rasat: SMT for polynomial inequality. In: Proceedings of the 12th International Workshop on Satisfiability Modulo Theories, SMT 2014, Vienna, Austria, July 17\u201318, 2014, p. 67 (2014)"},{"key":"8_CR29","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/BF02807438","volume":"12","author":"J-L Krivine","year":"1964","unstructured":"Krivine, J.-L.: Anneaux pr\u00e9ordonn\u00e9s. J. d\u2019 Anal. Math. 12, 307\u2013326 (1964)","journal-title":"J. d\u2019 Anal. Math."},{"key":"8_CR30","series-title":"Imperial College Optimization Series","volume-title":"Moments, Positive Polynomials and Their Applications","author":"JB Lasserre","year":"2010","unstructured":"Lasserre, J.B.: Moments, Positive Polynomials and Their Applications. Imperial College Optimization Series, vol. 1. Imperial College Press, London (2010)"},{"issue":"6","key":"8_CR31","doi-asserted-by":"publisher","first-page":"525","DOI":"10.1023\/A:1025117523902","volume":"2","author":"V Loechner","year":"1997","unstructured":"Loechner, V., Wilde, D.K.: Parameterized polyhedra and their vertices. Int. J. Parallel Program. 2(6), 525\u2013549 (1997). Tool available at \n                      icps.u-strasbg.fr\/polylib\/","journal-title":"Int. J. Parallel Program."},{"key":"8_CR32","unstructured":"Mar\u00e9chal, A., P\u00e9rin, M.: Three linearization techniques for multivariate polynomials in static analysis using convex polyhedra. Technical Report 7, Verimag, July 2014"},{"key":"8_CR33","unstructured":"Mar\u00e9chal, A., P\u00e9rin, M.: A linearization technique for multivariate polynomials using convex polyhedra based on Handelman\u2019s theorem. J. Francophones des Langages Applicatifs (JFLA), January 2015"},{"key":"8_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/11609773_23","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A Min\u00e9","year":"2006","unstructured":"Min\u00e9, A.: Symbolic methods to enhance the precision of numerical abstract domains. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 348\u2013363. Springer, Heidelberg (2006)"},{"issue":"2","key":"8_CR35","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/s10817-012-9256-3","volume":"51","author":"C Mu\u00f1oz","year":"2013","unstructured":"Mu\u00f1oz, C., Narkawicz, A.: Formalization of a representation of Bernstein polynomials and applications to global optimization. J. Autom. Reasoning 51(2), 151\u2013196 (2013)","journal-title":"J. Autom. Reasoning"},{"key":"8_CR36","unstructured":"N\u00e9ron, P.: A Quest for Exactness: Program Transformation for Reliable Real Numbers. Ph.D. thesis, \u00c9cole Polytechnique, Palaiseau, France (2013)"},{"key":"8_CR37","doi-asserted-by":"crossref","unstructured":"Prestel, A., Delzell, C.N.: Positive Polynomials: From Hilbert\u2019s 17th Problem to Real Algebra. Springer-Verlag, June 2001","DOI":"10.1007\/978-3-662-04648-7"},{"issue":"3","key":"8_CR38","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1016\/S0022-4049(01)00041-X","volume":"166","author":"M Schweighofer","year":"2002","unstructured":"Schweighofer, M.: An algorithmic approach to Schm\u00fcdgen\u2019s Positivstellensatz. J. Pure Appl. Algebra 166(3), 307\u2013319 (2002)","journal-title":"J. Pure Appl. Algebra"},{"key":"8_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"367","DOI":"10.1007\/978-3-319-08587-6_28","volume-title":"Automated Reasoning","author":"A Stump","year":"2014","unstructured":"Stump, A., Sutcliffe, G., Tinelli, C.: StarExec: a cross-community infrastructure for logic solving. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS, vol. 8562, pp. 367\u2013373. Springer, Heidelberg (2014)"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-49122-5_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T04:34:57Z","timestamp":1559363697000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-49122-5_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,12,25]]},"ISBN":["9783662491218","9783662491225"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-49122-5_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,12,25]]}}}