{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T20:12:56Z","timestamp":1774987976373,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642388552","type":"print"},{"value":"9783642388569","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-38856-9_19","type":"book-chapter","created":{"date-parts":[[2013,6,15]],"date-time":"2013-06-15T00:05:28Z","timestamp":1371254728000},"page":"345-365","source":"Crossref","is-referenced-by-count":22,"title":["Efficient Generation of Correctness Certificates for the Abstract Domain of Polyhedra"],"prefix":"10.1007","author":[{"given":"Alexis","family":"Fouilhe","sequence":"first","affiliation":[]},{"given":"David","family":"Monniaux","sequence":"additional","affiliation":[]},{"given":"Micha\u00ebl","family":"P\u00e9rin","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"19_CR1","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: Principles of Programming Languages (POPL), pp. 238\u2013252. ACM (1977)","DOI":"10.1145\/512950.512973"},{"key":"19_CR2","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Principles of Programming Languages (POPL), pp. 84\u201397. ACM (1978)","DOI":"10.1145\/512760.512770"},{"issue":"1-2","key":"19_CR3","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. Science of Computer Programming\u00a072(1-2), 3\u201321 (2008)","journal-title":"Science of Computer Programming"},{"key":"19_CR4","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.\u00a05643, pp. 661\u2013667. Springer, Heidelberg (2009)"},{"key":"19_CR5","doi-asserted-by":"crossref","unstructured":"Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: A static analyzer for large safety-critical software. In: Programming Language Design and Implementation (PLDI), pp. 196\u2013207. ACM (2003)","DOI":"10.1145\/780822.781153"},{"issue":"7","key":"19_CR6","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. Communications of the ACM\u00a052(7), 107\u2013115 (2009)","journal-title":"Communications of the ACM"},{"key":"19_CR7","unstructured":"The Coq Development Team: The Coq proof assistant reference manual. INRIA. 8.4. edn. (2012)"},{"key":"19_CR8","unstructured":"Besson, F., Jensen, T., Pichardie, D., Turpin, T.: Result certification for relational program analysis. Technical Report RR-6333, INRIA (2007)"},{"key":"19_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"336","DOI":"10.1007\/11547662_23","volume-title":"Static Analysis","author":"A. Simon","year":"2005","unstructured":"Simon, A., King, A.: Exploiting sparsity in polyhedral analysis. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol.\u00a03672, pp. 336\u2013351. Springer, Heidelberg (2005)"},{"key":"19_CR10","unstructured":"Dutertre, B., De Moura, L.: Integrating simplex with DPLL(T). Technical Report SRI-CSL-06-01, SRI International, computer science laboratory (2006)"},{"key":"19_CR11","doi-asserted-by":"crossref","unstructured":"Henry, J., Monniaux, D., Moy, M.: PAGAI: a path sensitive static analyser. In: Jeannet, B. (ed.) Tools for Automatic Program Analysis (TAPAS) (2012)","DOI":"10.1016\/j.entcs.2012.11.003"},{"issue":"2","key":"19_CR12","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/s10990-009-9046-8","volume":"22","author":"D. Monniaux","year":"2009","unstructured":"Monniaux, D.: A minimalistic look at widening operators. Higher Order and Symbolic Computation\u00a022(2), 145\u2013154 (2009)","journal-title":"Higher Order and Symbolic Computation"},{"key":"19_CR13","unstructured":"Dantzig, G., Thapa, M.N.D.: Linear Programming. Springer (2003)"},{"key":"19_CR14","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/10721959_3","volume-title":"Automated Deduction - CADE-17","author":"G.C. Necula","year":"2000","unstructured":"Necula, G.C., Lee, P.: Proof generation in the Touchstone theorem prover. In: McAllester, D. (ed.) CADE 2000. LNCS (LNAI), vol.\u00a01831, pp. 25\u201344. Springer, Heidelberg (2000)"},{"issue":"1-2","key":"19_CR15","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1017\/S1471068404002261","volume":"5","author":"F. Benoy","year":"2005","unstructured":"Benoy, F., King, A., Mesnard, F.: Computing convex hulls with a linear solver. Theory and Practice of Logic Programming\u00a05(1-2), 259\u2013271 (2005)","journal-title":"Theory and Practice of Logic Programming"},{"key":"19_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-14295-6_51","volume-title":"Computer Aided Verification","author":"D. Monniaux","year":"2010","unstructured":"Monniaux, D.: Quantifier elimination by lazy model enumeration. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 585\u2013599. Springer, Heidelberg (2010)"},{"issue":"1-2","key":"19_CR17","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1016\/j.scico.2005.02.003","volume":"58","author":"R. Bagnara","year":"2005","unstructured":"Bagnara, R., Hill, P.M., Ricci, E., Zaffanella, E.: Precise widening operators for convex polyhedra. Science of Computer Programming\u00a058(1-2), 28\u201356 (2005)","journal-title":"Science of Computer Programming"},{"key":"19_CR18","unstructured":"Min\u00e9, A., Leroy, X.: ZArith, \n                  \n                    http:\/\/forge.ocamlcore.org\/projects\/zarith"},{"key":"19_CR19","unstructured":"Free Software Foundation: The GNU Multiple Precision Arithmetic Library. 5.0 edn. (2012)"},{"key":"19_CR20","unstructured":"Barbosa, C., de Oliveira, D., Monniaux, D.: Experiments on the feasibility of using a floating-point simplex in an SMT solver. In: Workshop on Practical Aspects of Automated Reasoning (PAAR), CEUR Workshop Proceedings (2012)"},{"key":"19_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"570","DOI":"10.1007\/978-3-642-02658-4_42","volume-title":"Computer Aided Verification","author":"D. Monniaux","year":"2009","unstructured":"Monniaux, D.: On using floating-point computations to help an exact linear arithmetic decision procedure. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 570\u2013583. Springer, Heidelberg (2009)"},{"key":"19_CR22","unstructured":"Bugseng: The Parma Polyhedra Library. 1.0 edn. (2012)"},{"key":"19_CR23","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.\u00a03855, pp. 348\u2013363. Springer, Heidelberg (2006)"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-38856-9_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,14]],"date-time":"2019-05-14T00:48:38Z","timestamp":1557794918000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-38856-9_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642388552","9783642388569"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-38856-9_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}