{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:30:06Z","timestamp":1774837806550,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":48,"publisher":"ACM","license":[{"start":{"date-parts":[[2004,9,19]],"date-time":"2004-09-19T00:00:00Z","timestamp":1095552000000},"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":[[2004,9,19]]},"DOI":"10.1145\/1016850.1016875","type":"proceedings-article","created":{"date-parts":[[2004,10,7]],"date-time":"2004-10-07T13:39:48Z","timestamp":1097156388000},"page":"175-188","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":23,"title":["Verification of safety properties for concurrent assembly code"],"prefix":"10.1145","author":[{"given":"Dachuan","family":"Yu","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":[[2004,9,19]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/151646.151649"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/203095.201069"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/604174.604185"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/871816.871860"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/s002360050039"},{"key":"e_1_3_2_1_6_1","volume-title":"Extensible code verification. Unpublished manuscript","author":"Chang B.-Y. E.","year":"2003","unstructured":"B.-Y. E. Chang , G. C. Necular , and R. R. Schneck . Extensible code verification. Unpublished manuscript , 2003 . B.-Y. E. Chang, G. C. Necular, and R. R. Schneck. Extensible code verification. Unpublished manuscript, 2003."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/322108.322121"},{"key":"e_1_3_2_1_8_1","first-page":"89","volume-title":"Mathematical Logic and Programming Languages","author":"Clarke E. M.","year":"1985","unstructured":"E. M. Clarke . The characterization problem for Hoare logics . In C. A. R. Hoare and J. C. Shepherdson, editors, Mathematical Logic and Programming Languages , pages 89 -- 106 . Prentice Hall , 1985 . E. M. Clarke. The characterization problem for Hoare logics. In C. A. R. Hoare and J. C. Shepherdson, editors, Mathematical Logic and Programming Languages, pages 89--106. Prentice Hall, 1985."},{"key":"e_1_3_2_1_9_1","volume-title":"Concurrency Verification: Introduction to Compositional and Noncompositional Methods","author":"de Roever W.-P.","year":"2001","unstructured":"W.-P. de Roever , F. de Boer , U. Hannemann , J. Hooman , Y. Lakhnech , M. Poel , and J. Zwiers . Concurrency Verification: Introduction to Compositional and Noncompositional Methods . Cambridge University Press , Cambridge, UK , 2001 . W.-P. de Roever, F. de Boer, U. Hannemann, J. Hooman, Y. Lakhnech, M. Poel, and J. Zwiers. Concurrency Verification: Introduction to Compositional and Noncompositional Methods. Cambridge University Press, Cambridge, UK, 2001."},{"key":"e_1_3_2_1_10_1","first-page":"43","volume-title":"Programming Languages","author":"Dijsktra E. W.","year":"1968","unstructured":"E. W. Dijsktra . Cooperating sequential processes . In F. Genuys, editor, Programming Languages , pages 43 -- 112 . Academic Press , 1968 . E. W. Dijsktra. Cooperating sequential processes. In F. Genuys, editor, Programming Languages, pages 43--112. Academic Press, 1968."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/645396.651955"},{"key":"e_1_3_2_1_12_1","first-page":"19","volume-title":"Proceedings of the Symposium on Applied Math.","volume":"19","author":"Floyd R. W.","year":"1967","unstructured":"R. W. Floyd . Assigning meanings to programs. In A. M. Society, editor , Proceedings of the Symposium on Applied Math. Vol. 19 , pages 19 -- 31 , Providence, R.I. , 1967 . R. W. Floyd. Assigning meanings to programs. In A. M. Society, editor, Proceedings of the Symposium on Applied Math. Vol. 19, pages 19--31, Providence, R.I., 1967."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00289074"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292563"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/645683.664592"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/646185.683072"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/362452.362489"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/359576.359585"},{"key":"e_1_3_2_1_20_1","first-page":"262","volume-title":"Proc. 2003 International Conference on Compiler Construction (CC'03)","volume":"2622","author":"Hoare T.","year":"2003","unstructured":"T. Hoare . The verifying compiler: A grand challenge for computing research . In Proc. 2003 International Conference on Compiler Construction (CC'03) , LNCS Vol. 2622 , pages 262 -- 272 , Warsaw, Poland , Apr. 2003 . Springer-Verlag Heidelberg. T. Hoare. The verifying compiler: A grand challenge for computing research. In Proc. 2003 International Conference on Compiler Construction (CC'03), LNCS Vol. 2622, pages 262--272, Warsaw, Poland, Apr. 2003. Springer-Verlag Heidelberg."},{"key":"e_1_3_2_1_21_1","unstructured":"J. Hooman W.-P. de Roever P. Pandya Q. Xu P. Zhou and H. Schepers. A compositional approach to concurrency and its applications. Incomplete manuscript. http:\/\/www.informatik.uni-kiel.de\/inf\/deRoever\/books\/ Apr. 2003.  J. Hooman W.-P. de Roever P. Pandya Q. Xu P. Zhou and H. Schepers. A compositional approach to concurrency and its applications. Incomplete manuscript. http:\/\/www.informatik.uni-kiel.de\/inf\/deRoever\/books\/ Apr. 2003."},{"key":"e_1_3_2_1_22_1","first-page":"479","volume-title":"To H.B.Curry: Essays on Computational Logic, Lambda Calculus and Formalism","author":"Howard W. A.","year":"1980","unstructured":"W. A. Howard . The formulae-as-types notion of constructions . In To H.B.Curry: Essays on Computational Logic, Lambda Calculus and Formalism , pages 479 -- 490 . Academic Press , 1980 . W. A. Howard. The formulae-as-types notion of constructions. In To H.B.Curry: Essays on Computational Logic, Lambda Calculus and Formalism, pages 479--490. Academic Press, 1980."},{"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","doi-asserted-by":"publisher","DOI":"10.1145\/2993.357247"},{"key":"e_1_3_2_1_26_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_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1981.230844"},{"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\/238721.238781"},{"key":"e_1_3_2_1_30_1","first-page":"248","volume-title":"Proceedings of IEEE Symposium on Logic in Computer Science","author":"Necula G. C.","year":"2003","unstructured":"G. C. Necula and R. R. Schneck . A sound framework for untrustred verification-condition generators . In Proceedings of IEEE Symposium on Logic in Computer Science , pages 248 -- 260 . IEEE Computer Society , July 2003 . G. C. Necula and R. R. Schneck. A sound framework for untrustred verification-condition generators. In Proceedings of IEEE Symposium on Logic in Computer Science, pages 248--260. IEEE Computer Society, July 2003."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964024"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/69575.2083"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00268134"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/357172.357178"},{"key":"e_1_3_2_1_35_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 M. Bezem and J. Groote, editors, Proc. TLCA , volume 664 of LNCS . Springer-Verlag , 1993 . C. Paulin-Mohring. Inductive definitions in the system Coq-rules and properties. In M. Bezem and J. Groote, editors, Proc. TLCA, volume 664 of LNCS. Springer-Verlag, 1993."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1007\/978-3-642-82453-1_5","volume-title":"Logics and models of concurrent systems","author":"Pnueli A.","year":"1985","unstructured":"A. Pnueli . In transition from global to modular temporal reasoning about programs. Logics and models of concurrent systems , pages 123 -- 144 , 1985 . A. Pnueli. In transition from global to modular temporal reasoning about programs. Logics and models of concurrent systems, pages 123--144, 1985."},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/113445.113470"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.5555\/645683.664578"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503293"},{"key":"e_1_3_2_1_40_1","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"369","DOI":"10.1007\/3-540-16042-6_21","volume-title":"Proc. 5th Conference on Foundations of Software Technology and Theoretical Computer Science","author":"Stark E. W.","year":"1985","unstructured":"E. W. Stark . A proof technique for rely\/guarantee properties. In S. N. Maheshwari, editor, Proc. 5th Conference on Foundations of Software Technology and Theoretical Computer Science , volume 206 of LNCS , pages 369 -- 391 , New Delhi, 1985 . Springer-Verlag . E. W. Stark. A proof technique for rely\/guarantee properties. In S. N. Maheshwari, editor, Proc. 5th Conference on Foundations of Software Technology and Theoretical Computer Science, volume 206 of LNCS, pages 369--391, New Delhi, 1985. Springer-Verlag."},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(88)90033-3"},{"key":"e_1_3_2_1_42_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_43_1","unstructured":"The FLINT Project. Coq (v7.3.1) implementation for CCAP language soundness and examples. http:\/\/flint.cs.yale.edu\/flint\/publications\/vsca.html (17k) Mar. 2004.  The FLINT Project. Coq (v7.3.1) implementation for CCAP language soundness and examples. http:\/\/flint.cs.yale.edu\/flint\/publications\/vsca.html (17k) Mar. 2004."},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1093"},{"key":"e_1_3_2_1_45_1","first-page":"267","volume-title":"International Conference on Concurrency Theory","author":"Xu Q.","year":"1994","unstructured":"Q. Xu , A. Cau , and P. Collette . On unifying assumption-commitment style proof rules for concurrency . In International Conference on Concurrency Theory , pages 267 -- 282 , 1994 . Q. Xu, A. Cau, and P. Collette. On unifying assumption-commitment style proof rules for concurrency. In International Conference on Concurrency Theory, pages 267--282, 1994."},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.5555\/1765712.1765739"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2004.01.003"},{"key":"e_1_3_2_1_48_1","unstructured":"Y. Yu. Automated proofs of object code for a widely used microprocessor. PhD thesis University of Texas at Austin Austin TX 1992.   Y. Yu. Automated proofs of object code for a widely used microprocessor. PhD thesis University of Texas at Austin Austin TX 1992."}],"event":{"name":"ICFP04: ACM SIGPLAN International Conference on Functional Programming","location":"Snow Bird UT USA","acronym":"ICFP04","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","ACM Association for Computing Machinery"]},"container-title":["Proceedings of the ninth ACM SIGPLAN international conference on Functional programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1016850.1016875","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1016850.1016875","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T12:31:00Z","timestamp":1750249860000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1016850.1016875"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,9,19]]},"references-count":48,"alternative-id":["10.1145\/1016850.1016875","10.1145\/1016850"],"URL":"https:\/\/doi.org\/10.1145\/1016850.1016875","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/1016848.1016875","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2004,9,19]]},"assertion":[{"value":"2004-09-19","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}