{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:47:32Z","timestamp":1772164052748,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":25,"publisher":"ACM","license":[{"start":{"date-parts":[[2016,9,4]],"date-time":"2016-09-04T00:00:00Z","timestamp":1472947200000},"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":[[2016,9,4]]},"DOI":"10.1145\/2951913.2951937","type":"proceedings-article","created":{"date-parts":[[2016,8,29]],"date-time":"2016-08-29T08:17:16Z","timestamp":1472458636000},"page":"325-337","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["An abstract memory functor for verified C static analyzers"],"prefix":"10.1145","author":[{"given":"Sandrine","family":"Blazy","sequence":"first","affiliation":[{"name":"University of Rennes 1, France \/ IRISA, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vincent","family":"Laporte","sequence":"additional","affiliation":[{"name":"IMDEA Software Institute, Spain"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Pichardie","sequence":"additional","affiliation":[{"name":"ENS Rennes, France \/ IRISA, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2016,9,4]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"Companion website 2016. http:\/\/www.irisa.fr\/celtique\/ext\/ abstract-memory.  Companion website 2016. http:\/\/www.irisa.fr\/celtique\/ext\/ abstract-memory."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03153-3_4"},{"key":"e_1_3_2_1_3_1","first-page":"344","volume-title":"Proceddings of Static Analysis Symposium (SAS)","volume":"7935","author":"Blazy Sandrine","unstructured":"Sandrine Blazy , Vincent Laporte , Andr\u00e9 Maroneze , and David Pichardie . Formal verification of a C value analysis based on abstract interpretation . In Proceddings of Static Analysis Symposium (SAS) , volume 7935 of LNCS, pages 324\u2013 344 . Springer, 2013. Sandrine Blazy, Vincent Laporte, Andr\u00e9 Maroneze, and David Pichardie. Formal verification of a C value analysis based on abstract interpretation. In Proceddings of Static Analysis Symposium (SAS), volume 7935 of LNCS, pages 324\u2013344. Springer, 2013."},{"key":"e_1_3_2_1_4_1","series-title":"LNCS","first-page":"141","volume-title":"Proceedings of FMPA","author":"Bourdoncle Fran\u00e7ois","unstructured":"Fran\u00e7ois Bourdoncle . Efficient chaotic iteration strategies with widenings . In Proceedings of FMPA , volume 735 of LNCS , pages 128\u2013 141 . Springer, 1993. Fran\u00e7ois Bourdoncle. Efficient chaotic iteration strategies with widenings. In Proceedings of FMPA, volume 735 of LNCS, pages 128\u2013141. Springer, 1993."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.06.004"},{"key":"e_1_3_2_1_6_1","first-page":"130","volume-title":"Proceedings of the Second International Symposium on Programming","author":"Cousot Patrick","unstructured":"Patrick Cousot and Radhia Cousot . Static determination of dynamic properties of programs . In Proceedings of the Second International Symposium on Programming , pages 106\u2013 130 . Dunod, Paris, France, 1976. Patrick Cousot and Radhia Cousot. Static determination of dynamic properties of programs. In Proceedings of the Second International Symposium on Programming, pages 106\u2013130. Dunod, Paris, France, 1976."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/512760.512770"},{"key":"e_1_3_2_1_9_1","first-page":"30","volume-title":"Xavier Rival. The ASTR\u00c9E Analyser. In Proceedings of European Symposium On Programming (ESOP\u201905)","volume":"3444","author":"Cousot Patrick","unstructured":"Patrick Cousot , Radhia Cousot , J\u00e9r\u00f4me Feret , Laurent Mauborgne , Antoine Min\u00e9 , David Monniaux , and Xavier Rival. The ASTR\u00c9E Analyser. In Proceedings of European Symposium On Programming (ESOP\u201905) , volume 3444 of LNCS, pages 21\u2013 30 . Springer, 2005. Patrick Cousot, Radhia Cousot, J\u00e9r\u00f4me Feret, Laurent Mauborgne, Antoine Min\u00e9, David Monniaux, and Xavier Rival. The ASTR\u00c9E Analyser. In Proceedings of European Symposium On Programming (ESOP\u201905), volume 3444 of LNCS, pages 21\u201330. Springer, 2005."},{"key":"e_1_3_2_1_10_1","first-page":"365","volume-title":"Proceedings of Static Analysis Symposium (SAS)","volume":"7935","author":"Fouilh\u00e9 Alexis","unstructured":"Alexis Fouilh\u00e9 , David Monniaux , and Micha\u00ebl P\u00e9rin . Efficient generation of correctness certificates for the abstract domain of polyhedra . In Proceedings of Static Analysis Symposium (SAS) , volume 7935 of LNCS, pages 345\u2013 365 . Springer, 2013. Alexis Fouilh\u00e9, David Monniaux, and Micha\u00ebl P\u00e9rin. Efficient generation of correctness certificates for the abstract domain of polyhedra. In Proceedings of Static Analysis Symposium (SAS), volume 7935 of LNCS, pages 345\u2013365. Springer, 2013."},{"key":"e_1_3_2_1_11_1","first-page":"529","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"Gopan Denis","unstructured":"Denis Gopan , Frank DiMaio , Nurit Dor , Thomas Reps , and Mooly Sagiv . Numeric domains with summarized dimensions . In Tools and Algorithms for the Construction and Analysis of Systems (TACAS) , pages 512\u2013 529 . Springer, 2004. Denis Gopan, Frank DiMaio, Nurit Dor, Thomas Reps, and Mooly Sagiv. Numeric domains with summarized dimensions. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 512\u2013529. Springer, 2004."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1080\/00207168908803778"},{"key":"e_1_3_2_1_13_1","first-page":"192","volume-title":"Proceedings of TAPSOFT\u201991","author":"Granger Philippe","unstructured":"Philippe Granger . Static analysis of linear congruence equalities among variables of a program . In Proceedings of TAPSOFT\u201991 , pages 169\u2013 192 . Springer, 1991. Philippe Granger. Static analysis of linear congruence equalities among variables of a program. In Proceedings of TAPSOFT\u201991, pages 169\u2013192. Springer, 1991."},{"key":"e_1_3_2_1_14_1","volume-title":"Technical Report WG14 N1124","author":"ISO.","year":"1999","unstructured":"ISO. The ANSI C standard (C99). Technical Report WG14 N1124 , ISO\/IEC , 1999 . ISO. The ANSI C standard (C99). Technical Report WG14 N1124, ISO\/IEC, 1999."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676966"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00268497"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1146809.1146811"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9155-4"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35308-6_5"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1134650.1134659"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2013.01.007"},{"key":"e_1_3_2_1_24_1","series-title":"LNCS","first-page":"132","volume-title":"Proceedings of Interactive Theorem Proving (ITP)","author":"Nipkow Tobias","unstructured":"Tobias Nipkow . Abstract interpretation of annotated commands . In Proceedings of Interactive Theorem Proving (ITP) , volume 7406 of LNCS , pages 116\u2013 132 . Springer, 2012. Tobias Nipkow. Abstract interpretation of annotated commands. In Proceedings of Interactive Theorem Proving (ITP), volume 7406 of LNCS, pages 116\u2013132. Springer, 2012."},{"key":"e_1_3_2_1_25_1","volume-title":"Inria","author":"The","year":"2012","unstructured":"The Coq development team. The Coq proof assistant reference manual . Inria , 2012 . The Coq development team. The Coq proof assistant reference manual. Inria, 2012."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993532"}],"event":{"name":"ICFP'16: ACM SIGPLAN International Conference on Functional Programming","location":"Nara Japan","acronym":"ICFP'16","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2951913.2951937","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2951913.2951937","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:56:21Z","timestamp":1750208181000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2951913.2951937"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,9,4]]},"references-count":25,"alternative-id":["10.1145\/2951913.2951937","10.1145\/2951913"],"URL":"https:\/\/doi.org\/10.1145\/2951913.2951937","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/3022670.2951937","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2016,9,4]]},"assertion":[{"value":"2016-09-04","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}