{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T17:43:06Z","timestamp":1742924586586,"version":"3.40.3"},"publisher-location":"Cham","reference-count":20,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319221014"},{"type":"electronic","value":"9783319221021"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"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":[[2015]]},"DOI":"10.1007\/978-3-319-22102-1_7","type":"book-chapter","created":{"date-parts":[[2015,8,18]],"date-time":"2015-08-18T08:30:14Z","timestamp":1439886614000},"page":"100-116","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Refinement to Certify Abstract Interpretations, Illustrated on Linearization for Polyhedra"],"prefix":"10.1007","author":[{"given":"Sylvain","family":"Boulm\u00e9","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexandre","family":"Mar\u00e9chal","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,8,19]]},"reference":[{"key":"7_CR1","unstructured":"The Coq Development Team: The Coq proof assistant reference manual - version 8.4. INRIA (2012\u20132014)"},{"key":"7_CR2","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL. ACM (1977)","DOI":"10.1145\/512950.512973"},{"key":"7_CR3","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: POPL. ACM (1978)","DOI":"10.1145\/512760.512770"},{"key":"7_CR4","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)"},{"key":"7_CR5","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":"7_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1007\/978-3-319-12154-3_13","volume-title":"Verified Software: Theories, Tools and Experiments","author":"A Fouilhe","year":"2014","unstructured":"Fouilhe, A., Boulm\u00e9, S.: A certifying frontend for (sub) polyhedral abstract domains. In: Giannakopoulou, D., Kroening, D. (eds.) VSTTE 2014. LNCS, vol. 8471, pp. 200\u2013215. Springer, Heidelberg (2014)"},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"Jourdan, J.H., Laporte, V., Blazy, S., Leroy, X., Pichardie, D.: A formally-verified C static analyzer. In: POPL. ACM (2015)","DOI":"10.1145\/2676726.2676966"},{"key":"7_CR8","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52, 107\u2013115 (2009)","journal-title":"Commun. ACM"},{"key":"7_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/978-3-642-15640-3_17","volume-title":"Trustworthly Global Computing","author":"F Besson","year":"2010","unstructured":"Besson, F., Jensen, T., Pichardie, D., Turpin, T.: Certified result checking for polyhedral analysis of bytecode programs. In: Wirsing, M., Hofmann, M., Rauschmayer, A. (eds.) TGC 2010, LNCS, vol. 6084, pp. 253\u2013267. Springer, Heidelberg (2010)"},{"key":"7_CR10","unstructured":"Mar\u00e9chal, A., P\u00e9rin, M.: Three linearization techniques for multivariate polynomials in static analysis using convex polyhedra. Technical report TR-2014-7, Verimag Research Report (2014)"},{"key":"7_CR11","series-title":"Graduate Texts in Computer Science","volume-title":"Refinement Calculus - A Systematic Introduction","author":"RJ Back","year":"1999","unstructured":"Back, R.J., von Wright, J.: Refinement Calculus - A Systematic Introduction. Graduate Texts in Computer Science. Springer, Heidelberg (1999)"},{"key":"7_CR12","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/BF01019459","volume":"6","author":"JC Reynolds","year":"1993","unstructured":"Reynolds, J.C.: The discoveries of continuations. Lisp Symb. Comput. 6, 233\u2013247 (1993)","journal-title":"Lisp Symb. Comput."},{"key":"7_CR13","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1016\/S0304-3975(00)00313-3","volume":"277","author":"P Cousot","year":"2002","unstructured":"Cousot, P.: Constructive design of a hierarchy of semantics of a transition system by abstract interpretation. TCS 277, 47\u2013103 (2002)","journal-title":"TCS"},{"key":"7_CR14","unstructured":"Spiwack, A.: Abstract interpretation as anti-refinement. CoRR abs\/1310.4283 (2013)"},{"key":"7_CR15","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"EW Dijkstra","year":"1975","unstructured":"Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM 18, 453\u2013457 (1975)","journal-title":"Commun. ACM"},{"key":"7_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-59451-5_2","volume-title":"Advanced Functional Programming","author":"P Wadler","year":"1995","unstructured":"Wadler, P.: Monads for functional programming. In: Jeuring, J., Meijer, E. (eds.) AFP 1995. LNCS, vol. 925. Springer, Heidelberg (1995)"},{"key":"7_CR17","unstructured":"Boulm\u00e9, S., Mar\u00e9chal, A.: A refinement calculus to certify impure abstract computations of the verimag polyhedra library - documentation and Coq+OCaml sources (2015). http:\/\/www-verimag.imag.fr\/~boulme\/vpl201503"},{"key":"7_CR18","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1016\/j.cagd.2012.03.001","volume":"29","author":"RT Farouki","year":"2012","unstructured":"Farouki, R.T.: The Bernstein polynomial basis: a centennial retrospective. Comput. Aided Geom. Des. 29, 379\u2013419 (2012)","journal-title":"Comput. Aided Geom. Des."},{"key":"7_CR19","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, 35\u201362 (1988)","journal-title":"Pac. J. Math."},{"key":"7_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/11541868_7","volume-title":"Theorem Proving in Higher Order Logics","author":"B Gr\u00e9goire","year":"2005","unstructured":"Gr\u00e9goire, B., Mahboubi, A.: Proving equalities in a commutative ring done right in Coq. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 98\u2013113. Springer, Heidelberg (2005)"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-22102-1_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,21]],"date-time":"2023-02-21T06:01:35Z","timestamp":1676959295000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-22102-1_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319221014","9783319221021"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-22102-1_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"19 August 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}