{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T12:01:30Z","timestamp":1770292890903,"version":"3.49.0"},"reference-count":32,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2018,11,10]],"date-time":"2018-11-10T00:00:00Z","timestamp":1541808000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/100011199","name":"FP7 Ideas: European Research Council","doi-asserted-by":"publisher","award":["306595"],"award-info":[{"award-number":["306595"]}],"id":[{"id":"10.13039\/100011199","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2019,4]]},"DOI":"10.1007\/s10817-018-9492-2","type":"journal-article","created":{"date-parts":[[2018,11,10]],"date-time":"2018-11-10T08:46:47Z","timestamp":1541839607000},"page":"505-530","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Refinement to Certify Abstract Interpretations: Illustrated on Linearization for Polyhedra"],"prefix":"10.1007","volume":"62","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9501-9606","authenticated-orcid":false,"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":[[2018,11,10]]},"reference":[{"key":"9492_CR1","volume-title":"Refinement Calculus\u2014A Systematic Introduction. Graduate Texts in Computer Science","author":"RJ Back","year":"1999","unstructured":"Back, R.J., von Wright, J.: Refinement Calculus\u2014A Systematic Introduction. Graduate Texts in Computer Science. Springer, Berlin (1999)"},{"key":"9492_CR2","doi-asserted-by":"crossref","unstructured":"Besson, F., Jensen, T.P., Pichardie, D., Turpin, T.: Certified result checking for polyhedral analysis of bytecode programs. In: TGC, pp. 253\u2013267 (2010)","DOI":"10.1007\/978-3-642-15640-3_17"},{"key":"9492_CR3","doi-asserted-by":"crossref","unstructured":"Boulm\u00e9, S.: Intuitionistic refinement calculus. In: TLCA, LNCS, vol. 4583. Springer (2007)","DOI":"10.1007\/978-3-540-73228-0_6"},{"key":"9492_CR4","unstructured":"Boulm\u00e9, S.: What is the foreign function interface of the coq programming language? Talk at the coq workshop (2018). https:\/\/coqworkshop2018.inria.fr\/files\/2018\/07\/coq2018_talk_boulme.pdf"},{"key":"9492_CR5","doi-asserted-by":"crossref","unstructured":"Boulm\u00e9, S., Mar\u00e9chal, A.: Refinement to certify abstract interpretations, illustrated on linearization for polyhedra. In: ITP, LNCS, vol. 9236. Springer (2015)","DOI":"10.1007\/978-3-319-22102-1_7"},{"key":"9492_CR6","unstructured":"Boulm\u00e9, S., Mar\u00e9chal, A.: Toward certification for free! Preprint on HAL (2017). https:\/\/hal.archives-ouvertes.fr\/hal-01558252"},{"key":"9492_CR7","doi-asserted-by":"crossref","unstructured":"Braibant, T., Pous, D.: Deciding kleene algebras in coq. Log. Methods Comput. Sci. 8(1) (2012)","DOI":"10.2168\/LMCS-8(1:16)2012"},{"issue":"1\u20132","key":"9492_CR8","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(1\u20132), 47\u2013103 (2002)","journal-title":"TCS"},{"key":"9492_CR9","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":"9492_CR10","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"},{"issue":"8","key":"9492_CR11","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(8), 453\u2013457 (1975)","journal-title":"Commun. ACM"},{"issue":"6","key":"9492_CR12","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(6), 379\u2013419 (2012)","journal-title":"Comput. Aided Geom. Des."},{"key":"9492_CR13","doi-asserted-by":"crossref","unstructured":"Fouilh\u00e9, A., Boulm\u00e9, S.: A certifying frontend for (sub)polyhedral abstract domains. In: VSTTE, LNCS, vol. 8471. Springer (2014)","DOI":"10.1007\/978-3-319-12154-3_13"},{"key":"9492_CR14","doi-asserted-by":"crossref","unstructured":"Fouilh\u00e9, A., Monniaux, D., P\u00e9rin, M.: Efficient generation of correctness certificates for the abstract domain of polyhedra. In: SAS, vol. 7935. Springer (2013)","DOI":"10.1007\/978-3-642-38856-9_19"},{"key":"9492_CR15","doi-asserted-by":"crossref","unstructured":"Gr\u00e9goire, B., Mahboubi, A.: Proving equalities in a commutative ring done right in Coq. In: TPHOL, LNCS, vol. 3604, pp. 98\u2013113. Springer (2005)","DOI":"10.1007\/11541868_7"},{"issue":"1","key":"9492_CR16","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":"9492_CR17","unstructured":"Jourdan, J.H.: Verasco: a formally verified C static analyzer. Theses, Universite Paris Diderot-Paris VII (2016). https:\/\/hal.archives-ouvertes.fr\/tel-01327023"},{"key":"9492_CR18","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":"9492_CR19","unstructured":"Laporte, V.: Verified static analyzes for low-level languages. Theses, Universit\u00e9 Rennes 1 (2015). https:\/\/tel.archives-ouvertes.fr\/tel-01285624"},{"issue":"7","key":"9492_CR20","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(7), 107\u2013115 (2009)","journal-title":"Commun. ACM"},{"key":"9492_CR21","doi-asserted-by":"crossref","unstructured":"Liang, S., Hudak, P.: Modular denotational semantics for compiler construction. In: ESOP, vol. 1058, pp. 219\u2013234. Springer (1996)","DOI":"10.1007\/3-540-61055-3_39"},{"key":"9492_CR22","unstructured":"Mar\u00e9chal, A.: New algorithmics for polyhedral calculus via parametric linear programming. Ph.D. thesis, Universit\u00e9 Grenoble Alpes (2017)"},{"key":"9492_CR23","doi-asserted-by":"crossref","unstructured":"Mar\u00e9chal, A., Fouilh\u00e9, A., King, T., Monniaux, D., P\u00e9rin, M.: Polyhedral approximation of multivariate polynomials using Handelman\u2019s theorem. In: VMCAI, pp. 166\u2013184 (2016)","DOI":"10.1007\/978-3-662-49122-5_8"},{"key":"9492_CR24","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":"9492_CR25","doi-asserted-by":"crossref","unstructured":"Mauborgne, L., Rival, X.: Trace partitioning in abstract interpretation based static analyzers. In: ESOP\u201905, LNCS, vol. 3444 (2005)","DOI":"10.1007\/978-3-540-31987-0_2"},{"key":"9492_CR26","doi-asserted-by":"crossref","unstructured":"Min\u00e9, A.: Symbolic methods to enhance the precision of numerical abstract domains. In: VMCAI, LNCS, vol. 3855. Springer (2006)","DOI":"10.1007\/11609773_23"},{"key":"9492_CR27","volume-title":"Programming from Specifications. Prentice Hall International Series in Computer Science","author":"C Morgan","year":"1994","unstructured":"Morgan, C.: Programming from Specifications. Prentice Hall International Series in Computer Science, 2nd edn. Prentice Hall, Upper Saddle River (1994)","edition":"2"},{"key":"9492_CR28","doi-asserted-by":"crossref","unstructured":"Moscato, M.M., Mu\u00f1oz, C.A., Smith, A.P.: Affine arithmetic and applications to real-number proving. In: ITP, LNCS, vol. 9236. Springer (2015)","DOI":"10.1007\/978-3-319-22102-1_20"},{"issue":"3\u20134","key":"9492_CR29","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(3\u20134), 233\u2013247 (1993)","journal-title":"Lisp Symb. Comput."},{"key":"9492_CR30","unstructured":"Spiwack, A.: Abstract interpretation as anti-refinement. CoRR abs\/1310.4283 (2013). http:\/\/arxiv.org\/abs\/1310.4283"},{"key":"9492_CR31","unstructured":"The Coq Development Team: The Coq proof assistant reference manual\u2014version 8.4. INRIA (2012\u20132014)"},{"key":"9492_CR32","doi-asserted-by":"crossref","unstructured":"Wadler, P.: Monads for functional programming. In: AFP, LNCS, vol. 925. Springer (1995)","DOI":"10.1007\/3-540-59451-5_2"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-018-9492-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-018-9492-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-018-9492-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,5]],"date-time":"2022-09-05T19:04:54Z","timestamp":1662404694000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-018-9492-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,11,10]]},"references-count":32,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2019,4]]}},"alternative-id":["9492"],"URL":"https:\/\/doi.org\/10.1007\/s10817-018-9492-2","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,11,10]]},"assertion":[{"value":"22 October 2018","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"25 October 2018","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"10 November 2018","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}