{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:44:40Z","timestamp":1772163880630,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":34,"publisher":"ACM","license":[{"start":{"date-parts":[[2005,1,12]],"date-time":"2005-01-12T00:00:00Z","timestamp":1105488000000},"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,1,12]]},"DOI":"10.1145\/1040305.1040335","type":"proceedings-article","created":{"date-parts":[[2005,1,30]],"date-time":"2005-01-30T12:58:48Z","timestamp":1107089928000},"page":"364-377","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":84,"title":["Automated soundness proofs for dataflow analyses and transformations via local rules"],"prefix":"10.1145","author":[{"given":"Sorin","family":"Lerner","sequence":"first","affiliation":[{"name":"University of Washington"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Todd","family":"Millstein","sequence":"additional","affiliation":[{"name":"UCLA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Erika","family":"Rice","sequence":"additional","affiliation":[{"name":"University of Washington"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Craig","family":"Chambers","sequence":"additional","affiliation":[{"name":"University of Washington"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2005,1,12]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Proceedings of the 4th International Workshop on the Implementation of Logics (WIL'03)","author":"Aboul-Hosn Kamal","year":"2003","unstructured":"Kamal Aboul-Hosn and Dexter Kozen . KAT-ML : An interactive theorem prover for kleene algebra with tests . In Proceedings of the 4th International Workshop on the Implementation of Logics (WIL'03) , University of Manchester , September 2003 .]] Kamal Aboul-Hosn and Dexter Kozen. KAT-ML: An interactive theorem prover for kleene algebra with tests. In Proceedings of the 4th International Workshop on the Implementation of Logics (WIL'03), University of Manchester, September 2003.]]"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/647168.718144"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964003"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/781131.781144"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24725-8_27"},{"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.1145\/503272.503290"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/236337.236344"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512558"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/506315.506316"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01128407"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/0898-1221(94)00215-7"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/256167.256195"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503299"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503298"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/781131.781156"},{"key":"e_1_3_2_1_21_1","first-page":"25","volume-title":"1999 ACM SIGPLAN Workshop on Compiler Support for System Software","author":"Morrisett Greg","year":"1999","unstructured":"Greg Morrisett , Karl Crary , Neal Glew , Dan Grossman , Richard Samuels , Frederick Smith , David Walker , Stephanie Weirich , and Steve 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 .]] Greg Morrisett, Karl Crary, Neal Glew, Dan Grossman, Richard Samuels, Frederick Smith, David Walker, Stephanie Weirich, and Steve 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_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263712"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349314"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/277650.277752"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.5555\/646482.691453"},{"key":"e_1_3_2_1_26_1","volume-title":"Proceedings of the FLoC Workshop Run-Time Result Verification","author":"Rinard Martin","year":"1999","unstructured":"Martin Rinard and Darko Marinov . Credible compilation . In Proceedings of the FLoC Workshop Run-Time Result Verification , July 1999 .]] Martin Rinard and Darko Marinov. Credible compilation. In Proceedings of the FLoC Workshop Run-Time Result Verification, July 1999.]]"},{"key":"e_1_3_2_1_27_1","first-page":"189","volume-title":"Program Flow Analysis: Theory and Applications","author":"Sharir Micha","year":"1981","unstructured":"Micha Sharir and Amir Pnueli . Two approaches to interprocedural data flow analysis . In Steven~S. Muchnick and Neil~D. Jones, editors, Program Flow Analysis: Theory and Applications , chapter 7, pages 189 -- 233 . Prentice-hall , 1981 .]] Micha Sharir and Amir Pnueli. Two approaches to interprocedural data flow analysis. In Steven~S. Muchnick and Neil~D. Jones, editors, Program Flow Analysis: Theory and Applications, chapter 7, pages 189--233. Prentice-hall, 1981.]]"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/53990.54007"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964004"},{"key":"e_1_3_2_1_30_1","series-title":"Lecture Notes in Computer Science (LNCS)","doi-asserted-by":"crossref","first-page":"346","DOI":"10.1007\/3-540-54415-1_54","volume-title":"Theoretical Aspects of Computer Science (TACS), Sendai (Japan)","author":"Steffen Bernhard","year":"1991","unstructured":"Bernhard Steffen . Data flow analysis as model checking . In T. Ito and A.R. Meyer, editors, Theoretical Aspects of Computer Science (TACS), Sendai (Japan) , volume 526 of Lecture Notes in Computer Science (LNCS) , pages 346 -- 364 . Springer-Verlag , September 1991 .]] Bernhard Steffen. Data flow analysis as model checking. In T. Ito and A.R. Meyer, editors, Theoretical Aspects of Computer Science (TACS), Sendai (Japan), volume 526 of Lecture Notes in Computer Science (LNCS), pages 346--364. Springer-Verlag, September 1991.]]"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/231379.231414"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/143095.143120"},{"key":"e_1_3_2_1_33_1","volume-title":"Principles of Database and Knowledge-base Systems","author":"Ullman Jeffrey D.","year":"1988","unstructured":"Jeffrey D. Ullman . Principles of Database and Knowledge-base Systems , Volume I. Computer Science Press , 1988 .]] Jeffrey D. Ullman. Principles of Database and Knowledge-base Systems, Volume I. Computer Science Press, 1988.]]"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/996841.996859"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/267959.267960"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/158511.158642"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.5555\/83471.83479"}],"event":{"name":"POPL05: The 32nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages 2005","location":"Long Beach California USA","acronym":"POPL05","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","ACM Association for Computing Machinery","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1040305.1040335","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1040305.1040335","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T12:25:00Z","timestamp":1750249500000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1040305.1040335"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,1,12]]},"references-count":34,"alternative-id":["10.1145\/1040305.1040335","10.1145\/1040305"],"URL":"https:\/\/doi.org\/10.1145\/1040305.1040335","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/1047659.1040335","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2005,1,12]]},"assertion":[{"value":"2005-01-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}