{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T20:12:57Z","timestamp":1774987977905,"version":"3.50.1"},"publisher-location":"Cham","reference-count":16,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319121536","type":"print"},{"value":"9783319121543","type":"electronic"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"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":[[2014]]},"DOI":"10.1007\/978-3-319-12154-3_13","type":"book-chapter","created":{"date-parts":[[2014,10,13]],"date-time":"2014-10-13T08:20:23Z","timestamp":1413188423000},"page":"200-215","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":14,"title":["A Certifying Frontend for (Sub)polyhedral Abstract Domains"],"prefix":"10.1007","author":[{"given":"Alexis","family":"Fouilhe","sequence":"first","affiliation":[]},{"given":"Sylvain","family":"Boulm\u00e9","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2014,10,14]]},"reference":[{"key":"13_CR1","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: PLDI. ACM (2003)","DOI":"10.1145\/781131.781153"},{"key":"13_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"},{"issue":"7","key":"13_CR3","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":"13_CR4","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":"13_CR5","doi-asserted-by":"crossref","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)","DOI":"10.1016\/j.scico.2007.08.001"},{"key":"13_CR6","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":"13_CR7","unstructured":"Besson, F., Jensen, T., Pichardie, D., Turpin, T.: Result certification for relational program analysis. Technical report RR-6333, INRIA (2007)"},{"key":"13_CR8","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":"13_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/978-3-540-93900-9_20","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"V Laviron","year":"2009","unstructured":"Laviron, V., Logozzo, F.: SubPolyhedra: a (more) scalable approach to infer linear inequalities. In: Jones, N.D., M\u00fcller-Olm, M. (eds.) VMCAI 2009. LNCS, vol. 5403, pp. 229\u2013244. Springer, Heidelberg (2009)"},{"key":"13_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/11609773_8","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S Sankaranarayanan","year":"2006","unstructured":"Sankaranarayanan, S., Col\u00f3n, M.A., Sipma, H.B., Manna, Z.: Efficient strongly relational polyhedral analysis. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 111\u2013125. Springer, Heidelberg (2006)"},{"key":"13_CR11","unstructured":"Free Software Foundation: The GNU Multiple Precision Arithmetic Library, 5.0 edn. (2012)"},{"key":"13_CR12","unstructured":"Min\u00e9, A., Leroy, X.: ZArith. http:\/\/forge.ocamlcore.org\/projects\/zarith"},{"issue":"1","key":"13_CR13","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1017\/S0956796812000366","volume":"23","author":"F Pottier","year":"2013","unstructured":"Pottier, F.: Syntactic soundness proof of a type-and-capability system with hidden state. J. Funct. Program. 23(1), 38\u2013144 (2013)","journal-title":"J. Funct. Program."},{"key":"13_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/978-3-642-39634-2_8","volume-title":"Interactive Theorem Proving","author":"G Claret","year":"2013","unstructured":"Claret, G., Gonz\u00e1lez Huesca, L.D.C., R\u00e9gis-Gianas, Y., Ziliani, B.: Lightweight proof by reflection using a posteriori simulation of effectful computation. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 67\u201383. Springer, Heidelberg (2013)"},{"key":"13_CR15","doi-asserted-by":"crossref","unstructured":"Birkedal, L., Reus, B., Schwinghammer, J., St\u00f8vring, K., Thamsborg, J., Yang, H.: Step-indexed Kripke models over recursive worlds. In: POPL. ACM (2011)","DOI":"10.1145\/1926385.1926401"},{"key":"13_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1007\/978-3-642-38856-9_18","volume-title":"Static Analysis","author":"S Blazy","year":"2013","unstructured":"Blazy, S., Laporte, V., Maroneze, A., Pichardie, D.: Formal verification of a C value analysis based on abstract interpretation. In: Logozzo, F., F\u00e4hndrich, M. (eds.) Static Analysis. LNCS, vol. 7935, pp. 324\u2013344. Springer, Heidelberg (2013)"}],"container-title":["Lecture Notes in Computer Science","Verified Software: Theories, Tools and Experiments"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-12154-3_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,20]],"date-time":"2023-02-20T14:43:59Z","timestamp":1676904239000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-12154-3_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319121536","9783319121543"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-12154-3_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]},"assertion":[{"value":"14 October 2014","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}