{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T20:13:16Z","timestamp":1774987996706,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":30,"publisher":"ACM","license":[{"start":{"date-parts":[[2008,6,7]],"date-time":"2008-06-07T00:00:00Z","timestamp":1212796800000},"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":[[2008,6,7]]},"DOI":"10.1145\/1375581.1375603","type":"proceedings-article","created":{"date-parts":[[2008,6,10]],"date-time":"2008-06-10T10:13:22Z","timestamp":1213092802000},"page":"170-182","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":46,"title":["Certifying low-level programs with hardware interrupts and preemptive threads"],"prefix":"10.1145","author":[{"given":"Xinyu","family":"Feng","sequence":"first","affiliation":[{"name":"Toyota Technological Institute at Chicago, Chicago, IL, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhong","family":"Shao","sequence":"additional","affiliation":[{"name":"Yale University, New Haven, CT, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yuan","family":"Dong","sequence":"additional","affiliation":[{"name":"Tsinghua University, Beijing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yu","family":"Guo","sequence":"additional","affiliation":[{"name":"University of Science and Technology of China, Hefei, Anhui, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2008,6,7]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.41331"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040327"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1975.6312840"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-28644-8_2"},{"key":"e_1_3_2_1_5_1","volume-title":"The Coq proof assistant reference manual. The Coq release v8.1","author":"Team Coq Development","year":"2006","unstructured":"Coq Development Team . The Coq proof assistant reference manual. The Coq release v8.1 , 2006 . Coq Development Team. The Coq proof assistant reference manual. The Coq release v8.1, 2006."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378811"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1086365.1086399"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1133981.1134028"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/1762174.1762193"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190315.1190325"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/11541868_1"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/1784774.1784779"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/357980.358001"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/355620.361161"},{"key":"e_1_3_2_1_17_1","first-page":"61","volume-title":"Operating Systems Techniques","author":"Hoare C. A. R.","year":"1972","unstructured":"C. A. R. Hoare . Towards a theory of parallel programming . In Operating Systems Techniques , pages 61 -- 71 . Academic Press , 1972 . C. A. R. Hoare. Towards a theory of parallel programming. In Operating Systems Techniques, pages 61--71. Academic Press, 1972."},{"key":"e_1_3_2_1_18_1","first-page":"2008","volume-title":"Proc. 17th European Symp. on Prog. (ESOP'08)","author":"Hobor Aquinas","unstructured":"Aquinas Hobor , Andrew W. Appel , and Francesco Zappa Nardelli . Oracle semantics for concurrent separation logic . In Proc. 17th European Symp. on Prog. (ESOP'08) , page to appear, 2008 . Aquinas Hobor, Andrew W. Appel, and Francesco Zappa Nardelli. Oracle semantics for concurrent separation logic. In Proc. 17th European Symp. on Prog. (ESOP'08), page to appear, 2008."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.375719"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/358818.358824"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250788"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/268946.268954"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792233.1792248"},{"key":"e_1_3_2_1_25_1","first-page":"49","volume-title":"Proc. 15th Int'l Conf. on Concurrency Theory (CONCUR'04)","volume":"3170","author":"O'Hearn Peter W.","year":"2004","unstructured":"Peter W. O'Hearn . Resources, concurrency and local reasoning . In Proc. 15th Int'l Conf. on Concurrency Theory (CONCUR'04) , volume 3170 of LNCS, pages 49 -- 67 . Springer , September 2004 . Peter W. O'Hearn. Resources, concurrency and local reasoning. In Proc. 15th Int'l Conf. on Concurrency Theory (CONCUR'04), volume 3170 of LNCS, pages 49--67. Springer, September 2004."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964024"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.5555\/646847.707120"},{"key":"e_1_3_2_1_28_1","volume-title":"The Verisoft XT project. URL: http:\/\/www.verisoft.de","author":"Paul Wolfgang","year":"2007","unstructured":"Wolfgang Paul , Manfred Broy , and Thomas In der Rieden . The Verisoft XT project. URL: http:\/\/www.verisoft.de , 2007 . Wolfgang Paul, Manfred Broy, and Thomas In der Rieden. The Verisoft XT project. URL: http:\/\/www.verisoft.de, 2007."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.04.002"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/645683.664578"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.5555\/1762174.1762219"},{"key":"e_1_3_2_1_32_1","volume-title":"10th Workshop on Hot Topics in Operating Systems","author":"Tuch Harvey","year":"2005","unstructured":"Harvey Tuch , Gerwin Klein , and Gernot Heiser . OS verification -- now! In Proc . 10th Workshop on Hot Topics in Operating Systems , June 2005 . Harvey Tuch, Gerwin Klein, and Gernot Heiser. OS verification -- now! In Proc. 10th Workshop on Hot Topics in Operating Systems, June 2005."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.5555\/2392200.2392220"}],"event":{"name":"PLDI '08: ACM SIGPLAN Conference on Programming Language Design and Implementation","location":"Tucson AZ USA","acronym":"PLDI '08","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","ACM Association for Computing Machinery"]},"container-title":["Proceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1375581.1375603","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1375581.1375603","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T10:47:17Z","timestamp":1750243637000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1375581.1375603"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,6,7]]},"references-count":30,"alternative-id":["10.1145\/1375581.1375603","10.1145\/1375581"],"URL":"https:\/\/doi.org\/10.1145\/1375581.1375603","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/1379022.1375603","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2008,6,7]]},"assertion":[{"value":"2008-06-07","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}