{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:30:45Z","timestamp":1774837845719,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":41,"publisher":"ACM","license":[{"start":{"date-parts":[[2005,9,12]],"date-time":"2005-09-12T00:00:00Z","timestamp":1126483200000},"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":[[2005,9,12]]},"DOI":"10.1145\/1086365.1086399","type":"proceedings-article","created":{"date-parts":[[2005,11,7]],"date-time":"2005-11-07T12:34:39Z","timestamp":1131366879000},"page":"254-267","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":31,"title":["Modular verification of concurrent assembly code with dynamic thread creation and termination"],"prefix":"10.1145","author":[{"given":"Xinyu","family":"Feng","sequence":"first","affiliation":[{"name":"Yale University, New Haven, CT"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhong","family":"Shao","sequence":"additional","affiliation":[{"name":"Yale University, New Haven, CT"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2005,9,12]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/203095.201069"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/871816.871860"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040327"},{"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","doi-asserted-by":"publisher","DOI":"10.5555\/776816.776863"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349315"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90005-3"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604149"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/645879.672057"},{"key":"e_1_3_2_1_10_1","unstructured":"R. Ferreira and X. Feng. Coq (v8.0) implementation for CMAP language and the soundness proof. http:\/\/flint.cs.yale.edu\/publications\/cmap.html Mar. 2005.]]  R. Ferreira and X. Feng. Coq (v8.0) implementation for CMAP language and the soundness proof. http:\/\/flint.cs.yale.edu\/publications\/cmap.html Mar. 2005.]]"},{"key":"e_1_3_2_1_11_1","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"288","DOI":"10.1007\/3-540-48320-9_21","volume-title":"CONCUR'99 - Concurrency Theory","author":"Flanagan C.","year":"1999","unstructured":"C. Flanagan and M. Abadi . Object types against races . In CONCUR'99 - Concurrency Theory , volume 1664 of LNCS , pages 288 -- 303 . Springer-Verlag , 1999 .]] C. Flanagan and M. Abadi. Object types against races. In CONCUR'99 - Concurrency Theory, volume 1664 of LNCS, pages 288--303. Springer-Verlag, 1999.]]"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/645393.651882"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/645396.651955"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44829-2_14"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/781131.781169"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/786769.787035"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/604174.604177"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/645683.664592"},{"key":"e_1_3_2_1_19_1","volume-title":"Model checking Java programs using Java pathfinder. Software Tools for Technology Transfer (STTT), 2(4):72--84","author":"Havelund K.","year":"2000","unstructured":"K. Havelund and T. Pressburger . Model checking Java programs using Java pathfinder. Software Tools for Technology Transfer (STTT), 2(4):72--84 , 2000 .]] K. Havelund and T. Pressburger. Model checking Java programs using Java pathfinder. Software Tools for Technology Transfer (STTT), 2(4):72--84, 2000.]]"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/996841.996844"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/359576.359585"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/646730.703666"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/69575.69577"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177726"},{"key":"e_1_3_2_1_25_1","volume-title":"A Calculus of Communicating Systems","author":"Milner R.","year":"1982","unstructured":"R. Milner . A Calculus of Communicating Systems . Springer-Verlag New York, Inc. , 1982 .]] R. Milner. A Calculus of Communicating Systems. Springer-Verlag New York, Inc., 1982.]]"},{"key":"e_1_3_2_1_26_1","first-page":"25","volume-title":"1999 ACM SIGPLAN Workshop on Compiler Support for System Software","author":"Morrisett G.","year":"1999","unstructured":"G. Morrisett , K. Crary , N. Glew , D. Grossman , R. Samuels , F. Smith , D. Walker , S. Weirich , and S. Zdancewic . TALx86: a realistic typed assembly language . In 1999 ACM SIGPLAN Workshop on Compiler Support for System Software , pages 25 -- 35 , Atlanta, GA , May 1999 .]] G. Morrisett, K. Crary, N. Glew, D. Grossman, R. Samuels, F. Smith, D. Walker, S. Weirich, and S. Zdancewic. TALx86: a realistic typed assembly language. In 1999 ACM SIGPLAN Workshop on Compiler Support for System Software, pages 25--35, Atlanta, GA, May 1999.]]"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/268946.268954"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263712"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/277650.277752"},{"key":"e_1_3_2_1_30_1","volume-title":"Dec.","author":"Ni Z.","year":"2004","unstructured":"Z. Ni and Z. Shao . Certified assembly programming with embedded code pointers. Technical report , Dec. 2004 . http:\/\/flint.cs.yale.edu\/publications\/ecap.html.]] Z. Ni and Z. Shao. Certified assembly programming with embedded code pointers. Technical report, Dec. 2004. http:\/\/flint.cs.yale.edu\/publications\/ecap.html.]]"},{"key":"e_1_3_2_1_31_1","first-page":"49","volume-title":"Proc. 15th International Conference on Concurrency Theory (CONCUR'04)","volume":"3170","author":"O'Hearn P. W.","year":"2004","unstructured":"P. W. O'Hearn . Resources, concurrency and local reasoning . In Proc. 15th International Conference on Concurrency Theory (CONCUR'04) , volume 3170 of LNCS, pages 49 -- 67 , 2004 .]] P. W. O'Hearn. Resources, concurrency and local reasoning. In Proc. 15th International Conference on Concurrency Theory (CONCUR'04), volume 3170 of LNCS, pages 49--67, 2004.]]"},{"key":"e_1_3_2_1_32_1","series-title":"LNCS","volume-title":"Proc. TLCA","author":"Paulin-Mohring C.","year":"1993","unstructured":"C. Paulin-Mohring . Inductive definitions in the system Coq-rules and properties . In Proc. TLCA , volume 664 of LNCS , 1993 .]] C. Paulin-Mohring. Inductive definitions in the system Coq-rules and properties. In Proc. TLCA, volume 664 of LNCS, 1993.]]"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31980-1_7"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/113445.113470"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.5555\/646823.706907"},{"key":"e_1_3_2_1_36_1","first-page":"510","volume-title":"Proc. 2nd International Conference on Concurrency Theory (CONCUR'91)","author":"St\u00f8len K.","year":"1991","unstructured":"K. St\u00f8len . A method for the development of totally correct sharedstate parallel programs . In Proc. 2nd International Conference on Concurrency Theory (CONCUR'91) , pages 510 -- 525 , 1991 .]] K. St\u00f8len. A method for the development of totally correct sharedstate parallel programs. In Proc. 2nd International Conference on Concurrency Theory (CONCUR'91), pages 510--525, 1991.]]"},{"key":"e_1_3_2_1_37_1","volume-title":"Oct.","author":"Development Team The Coq","year":"2001","unstructured":"The Coq Development Team . The Coq proof assistant reference manual. The Coq release v7.1 , Oct. 2001 .]] The Coq Development Team. The Coq proof assistant reference manual. The Coq release v7.1, Oct. 2001.]]"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1093"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360206"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.5555\/1765712.1765739"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/1016850.1016875"}],"event":{"name":"ICFP05: ACM SIGPLAN International Conference on Functional Programming","location":"Tallinn Estonia","acronym":"ICFP05","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","ACM Association for Computing Machinery"]},"container-title":["Proceedings of the tenth ACM SIGPLAN international conference on Functional programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1086365.1086399","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1086365.1086399","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T12:08:12Z","timestamp":1750248492000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1086365.1086399"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,9,12]]},"references-count":41,"alternative-id":["10.1145\/1086365.1086399","10.1145\/1086365"],"URL":"https:\/\/doi.org\/10.1145\/1086365.1086399","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/1090189.1086399","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2005,9,12]]},"assertion":[{"value":"2005-09-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}