{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,12]],"date-time":"2026-06-12T04:36:01Z","timestamp":1781238961755,"version":"3.54.1"},"publisher-location":"New York, NY, USA","reference-count":36,"publisher":"ACM","license":[{"start":{"date-parts":[[2015,1,14]],"date-time":"2015-01-14T00:00:00Z","timestamp":1421193600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001665","name":"Agence Nationale de la Recherche","doi-asserted-by":"publisher","award":["ANR-11-INSE-003"],"award-info":[{"award-number":["ANR-11-INSE-003"]}],"id":[{"id":"10.13039\/501100001665","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2015,1,14]]},"DOI":"10.1145\/2676726.2676966","type":"proceedings-article","created":{"date-parts":[[2014,12,19]],"date-time":"2014-12-19T08:51:05Z","timestamp":1418979065000},"page":"247-259","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":74,"title":["A Formally-Verified C Static Analyzer"],"prefix":"10.1145","author":[{"given":"Jacques-Henri","family":"Jourdan","sequence":"first","affiliation":[{"name":"Inria, Le Chesnay, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Vincent","family":"Laporte","sequence":"additional","affiliation":[{"name":"IRISA & U. Rennes 1, Rennes, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sandrine","family":"Blazy","sequence":"additional","affiliation":[{"name":"IRISA & U. Rennes 1, Rennes, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Xavier","family":"Leroy","sequence":"additional","affiliation":[{"name":"Inria, Le Chesnay, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"David","family":"Pichardie","sequence":"additional","affiliation":[{"name":"IRISA & ENS Rennes, Rennes, France"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2015,1,14]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1709093.1709094"},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/2670099"},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792233.1792236"},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/504709.504712"},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03153-3_4"},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/781131.781153"},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/11813040_31"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38856-9_18"},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/ARITH.2011.40"},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-014-9306-0"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.06.004"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796808006904"},{"key":"e_1_3_2_2_13_1","volume-title":"SparrowBerry: A verified validator for an industrial-strength static analyzer.texttthttp:\/\/ropas.snu.ac.kr\/sparrowberry\/","author":"Cho S.","year":"2013","unstructured":"S. Cho , J. Kang , J. Choi , C.-K. Hur , and K. Yi . SparrowBerry: A verified validator for an industrial-strength static analyzer.texttthttp:\/\/ropas.snu.ac.kr\/sparrowberry\/ , 2013 . S. Cho, J. Kang, J. Choi, C.-K. Hur, and K. Yi. SparrowBerry: A verified validator for an industrial-strength static analyzer.texttthttp:\/\/ropas.snu.ac.kr\/sparrowberry\/, 2013."},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/567752.567778"},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-009-0089-6"},{"key":"e_1_3_2_2_17_1","series-title":"LNCS","first-page":"272","volume-title":"ASIAN","author":"Cousot P.","year":"2006","unstructured":"P. Cousot , R. Cousot , J. Feret , L. Mauborgne , A. Min\u00e9 , D. Monniaux , and X. Rival . Combination of abstractions in the Astr\u00e9e static analyzer . In ASIAN , volume 4435 of LNCS , pages 272 -- 300 . Springer , 2006 . P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Min\u00e9, D. Monniaux, and X. Rival. Combination of abstractions in the Astr\u00e9e static analyzer. In ASIAN, volume 4435 of LNCS, pages 272--300. Springer, 2006."},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38856-9_19"},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-12154-3_13"},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32347-8_8"},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30538-5_26"},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375623"},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27705-4_2"},{"key":"e_1_3_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/1882094.1882115"},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1146809.1146811"},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9155-4"},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-006-8609-1"},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/11609773_23"},{"key":"e_1_3_2_2_30_1","volume-title":"R\u00e9alisation m\u00e9canis\u00e9e d'interpr\u00e9teurs abstraits. Master's thesis","author":"Monniaux D.","year":"1998","unstructured":"D. Monniaux . R\u00e9alisation m\u00e9canis\u00e9e d'interpr\u00e9teurs abstraits. Master's thesis , U. Paris 7, 1998 . D. Monniaux. R\u00e9alisation m\u00e9canis\u00e9e d'interpr\u00e9teurs abstraits. Master's thesis, U. Paris 7, 1998."},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35182-2_9"},{"key":"e_1_3_2_2_32_1","volume-title":"Principles of Program Analysis","author":"Nielson F.","year":"2005","unstructured":"F. Nielson , H. Nielson , and C. Hankin . Principles of Program Analysis . Springer , 2005 . F. Nielson, H. Nielson, and C. Hankin. Principles of Program Analysis. Springer, 2005."},{"key":"e_1_3_2_2_33_1","series-title":"LNCS","first-page":"116","volume-title":"ITP","author":"Nipkow T.","year":"2012","unstructured":"T. Nipkow . Abstract interpretation of annotated commands. In ITP , volume 7406 of LNCS , pages 116 -- 132 . Springer , 2012 . T. Nipkow. Abstract interpretation of annotated commands. In ITP, volume 7406 of LNCS, pages 116--132. Springer, 2012."},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.04.064"},{"key":"e_1_3_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111542.1111560"},{"key":"e_1_3_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1275497.1275501"}],"event":{"name":"POPL '15: The 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","location":"Mumbai India","acronym":"POPL '15","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2676726.2676966","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2676726.2676966","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:13:03Z","timestamp":1750212783000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2676726.2676966"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,1,14]]},"references-count":36,"alternative-id":["10.1145\/2676726.2676966","10.1145\/2676726"],"URL":"https:\/\/doi.org\/10.1145\/2676726.2676966","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2775051.2676966","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2015,1,14]]},"assertion":[{"value":"2015-01-14","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}