{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,22]],"date-time":"2026-09-22T10:34:08Z","timestamp":1790073248705,"version":"4.0.1"},"publisher-location":"New York, NY, USA","reference-count":34,"publisher":"ACM","license":[{"start":{"date-parts":[[2003,5,9]],"date-time":"2003-05-09T00:00:00Z","timestamp":1052438400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2003,5,9]]},"DOI":"10.1145\/781131.781153","type":"proceedings-article","created":{"date-parts":[[2004,4,19]],"date-time":"2004-04-19T13:18:43Z","timestamp":1082380723000},"page":"196-207","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":384,"title":["A static analyzer for large safety-critical software"],"prefix":"10.1145","author":[{"given":"Bruno","family":"Blanchet","sequence":"first","affiliation":[{"name":"CNRS (Centre National de la Recherche Scientifique) and \u00c9cole normale sup\u00e9rieure"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Patrick","family":"Cousot","sequence":"additional","affiliation":[{"name":"\u00c9cole normale sup\u00e9rieure"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Radhia","family":"Cousot","sequence":"additional","affiliation":[{"name":"CNRS (Centre National de la Recherche Scientifique) and \u00c9cole polytechnique"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"J\u00e9rome","family":"Feret","sequence":"additional","affiliation":[{"name":"\u00c9cole normale sup\u00e9rieure"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Laurent","family":"Mauborgne","sequence":"additional","affiliation":[{"name":"\u00c9cole normale sup\u00e9rieure"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Antoine","family":"Min\u00e9","sequence":"additional","affiliation":[{"name":"\u00c9cole normale sup\u00e9rieure"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"David","family":"Monniaux","sequence":"additional","affiliation":[{"name":"CNRS (Centre National de la Recherche Scientifique) and \u00c9cole normale sup\u00e9rieure"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Xavier","family":"Rival","sequence":"additional","affiliation":[{"name":"\u00c9cole normale sup\u00e9rieure"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2003,5,9]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/647171.716103"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/381694.378846"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/646486.694618"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503274"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/860256.860262"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/645847.668649"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/567752.567778"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(92)90030-7"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/2.4.511"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/646448.692441"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/512760.512770"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512538"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/1251229.1251230"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/646787.703893"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/543552.512558"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/647170.718288"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/647766.733618"},{"key":"e_1_3_2_1_20_1","volume-title":"The synchronous dataflow programming language Lustre. phProc. of the IEEE 79, 9","author":"Halbwachs N.","year":"1991","unstructured":"N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud. The synchronous dataflow programming language Lustre. phProc. of the IEEE 79, 9 (1991), 1305--1320.]]"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503279"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"e_1_3_2_1_23_1","first-page":"745","article-title":"IEEE standard for binary floating-point arithmetic. Tech. rep","author":"IEEE Computer Society","year":"1985","unstructured":"IEEE Computer Society. IEEE standard for binary floating-point arithmetic. Tech. rep., ANSI\/IEEE Std 745-1985, 1985.]]","journal-title":"ANSI\/IEEE Std"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","unstructured":"G. Kildall. A unified approach to global program optimization. 1st ACM POPL (1973.) 194--206.]] 10.1145\/512927.512945","DOI":"10.1145\/512927.512945"},{"key":"e_1_3_2_1_25_1","volume-title":"INRIA","author":"Leroy X.","year":"2002","unstructured":"X. Leroy, D. Doligez, J. Garrigue, D. R\u00e9my, and J. Vouillon. The Objective Caml system, documentation and user's manual (release 3.06). Tech. rep., INRIA, Rocquencourt, France, 2002.]]"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/647171.716101"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.5555\/647171.718314"},{"key":"e_1_3_2_1_28_1","unstructured":"A. Min\u00e9. The octagon abstract domain library. http:\/\/www.di.ens.fr\/ mine\/oct\/.]]"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/645774.668110"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/832308.837141"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.5555\/1060289.1060297"},{"key":"e_1_3_2_1_32_1","volume-title":"PVS: An experience report. FM-Trends'98","author":"Owre S.","year":"1999","unstructured":"S. Owre, N. Shankar, and D. Stringer-Calvert. PVS: An experience report. FM-Trends'98 (1999), LNCS 1641, Springer, 117--132.]]"},{"key":"e_1_3_2_1_33_1","volume-title":"INRIA","author":"Development Team The Coq","year":"2003","unstructured":"The Coq Development Team. The Coq proof assistant reference manual (version 7.4). Tech. rep., INRIA, Rocquencourt, France, 2003.]]"},{"key":"e_1_3_2_1_34_1","volume-title":"Program slicing. phIEEE Transactions on Software Engineering SE-10, 4","author":"Weiser M.","year":"1984","unstructured":"M. Weiser. Program slicing. phIEEE Transactions on Software Engineering SE-10, 4 (1984), 352--357.]]"}],"event":{"name":"PLDI03: ACM SIGPLAN Conference on Programming Language Design and Implementation","location":"San Diego California USA","acronym":"PLDI03","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","ACM Association for Computing Machinery"]},"container-title":["Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/781131.781153","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/781131.781153","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T13:44:02Z","timestamp":1750254242000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/781131.781153"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,5,9]]},"references-count":34,"aliases":["10.1145\/781151.781153"],"alternative-id":["10.1145\/781131.781153","10.1145\/781131"],"URL":"https:\/\/doi.org\/10.1145\/781131.781153","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/780822.781153","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2003,5,9]]},"assertion":[{"value":"2003-05-09","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}