{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,29]],"date-time":"2026-05-29T12:15:41Z","timestamp":1780056941468,"version":"3.54.0"},"publisher-location":"New York, NY, USA","reference-count":14,"publisher":"ACM","license":[{"start":{"date-parts":[[2005,9,5]],"date-time":"2005-09-05T00:00:00Z","timestamp":1125878400000},"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,5]]},"DOI":"10.1145\/1108792.1108813","type":"proceedings-article","created":{"date-parts":[[2006,2,6]],"date-time":"2006-02-06T10:52:40Z","timestamp":1139223160000},"page":"82-87","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":115,"title":["Weakest-precondition of unstructured programs"],"prefix":"10.1145","author":[{"given":"Mike","family":"Barnett","sequence":"first","affiliation":[{"name":"Microsoft Research, Redmond, WA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"K. Rustan M.","family":"Leino","sequence":"additional","affiliation":[{"name":"Microsoft Research, Redmond, WA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2005,9,5]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Compilers: Principles, Techniques, and Tools","author":"Aho Alfred V.","year":"1987","unstructured":"Alfred V. Aho , Ravi Sethi , and Jeffrey D. Ullman . Compilers: Principles, Techniques, and Tools . Addison-Wesley , 1987 . Alfred V. Aho, Ravi Sethi, and Jeffrey D. Ullman. Compilers: Principles, Techniques, and Tools. Addison-Wesley, 1987."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF03037485"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30569-9_3"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"crossref","unstructured":"L.\n      Burdy A.\n      Requet and \n      J.-L.\n      Lanet\n    .\n  Java applet correctness: a developer-oriented approach\n  . In Keijiro Araki Stefania Gnesi and Dino Mandrioli editors FME \n  2003\n  : Formal Methods International Symposium of Formal Methods Europe volume \n  2805\n   of \n  LNCS pages \n  422\n  --\n  439\n  . \n  Springer September 2003.  L. Burdy A. Requet and J.-L. Lanet. Java applet correctness: a developer-oriented approach. In Keijiro Araki Stefania Gnesi and Dino Mandrioli editors FME 2003: Formal Methods International Symposium of Formal Methods Europe volume 2805 of LNCS pages 422--439. Springer September 2003.","DOI":"10.1007\/978-3-540-45236-2_24"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/115372.115320"},{"key":"e_1_3_2_1_9_1","volume-title":"A Discipline of Programming","author":"Dijkstra Edsger W.","year":"1976","unstructured":"Edsger W. Dijkstra . A Discipline of Programming . Prentice Hall , Englewood Cliffs, NJ , 1976 . Edsger W. Dijkstra. A Discipline of Programming. Prentice Hall, Englewood Cliffs, NJ, 1976."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/49418"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512558"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360220"},{"key":"e_1_3_2_1_13_1","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"104","DOI":"10.1007\/3-540-44829-2_7","volume-title":"Model Checking Software: SPIN","author":"Leino K. Rustan M.","year":"2003","unstructured":"K. Rustan M. Leino . A SAT characterization of boolean-program correctness . In Thomas Ball and Sriram K. Rajamani, editors, Model Checking Software: SPIN 2003 , volume 2648 of LNCS , pages 104 -- 120 . Springer , May 2003. K. Rustan M. Leino. A SAT characterization of boolean-program correctness. In Thomas Ball and Sriram K. Rajamani, editors, Model Checking Software: SPIN 2003, volume 2648 of LNCS, pages 104--120. Springer, May 2003."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2004.10.015"},{"key":"e_1_3_2_1_17_1","volume-title":"Geometric model checking: An automatic verification technique for loop and data reuse transformations. Electronic Notes Theoretical Computer Science, 65(2)","author":"Shashidhar K. C.","year":"2002","unstructured":"K. C. Shashidhar , Maurice Bruynooghe , Francky Catthoor , and Gerda Janssens . Geometric model checking: An automatic verification technique for loop and data reuse transformations. Electronic Notes Theoretical Computer Science, 65(2) , 2002 . K. C. Shashidhar, Maurice Bruynooghe, Francky Catthoor, and Gerda Janssens. Geometric model checking: An automatic verification technique for loop and data reuse transformations. Electronic Notes Theoretical Computer Science, 65(2), 2002."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1955.5.285"},{"key":"e_1_3_2_1_19_1","series-title":"LNCS","first-page":"299","volume-title":"Tiziana Margaria and Wang Yi","author":"van den Berg Joachim","year":"2001","unstructured":"Joachim van den Berg and Bart Jacobs . The LOOP compiler for Java and JML . In Tiziana Margaria and Wang Yi , editors, Tools and Algorithms for the Construction and Analysis of Systems, 7th International Conference, TACAS 2001 , volume 2031 of LNCS , pages 299 -- 312 . Springer , April 2001. Joachim van den Berg and Bart Jacobs. The LOOP compiler for Java and JML. In Tiziana Margaria and Wang Yi, editors, Tools and Algorithms for the Construction and Analysis of Systems, 7th International Conference, TACAS 2001, volume 2031 of LNCS, pages 299--312. Springer, April 2001."}],"event":{"name":"PASTE05: PASTE '05 - ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering","location":"Lisbon Portugal","acronym":"PASTE05","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGSOFT ACM Special Interest Group on Software Engineering"]},"container-title":["Proceedings of the 6th ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1108792.1108813","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1108792.1108813","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T12:07:50Z","timestamp":1750248470000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1108792.1108813"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,9,5]]},"references-count":14,"alternative-id":["10.1145\/1108792.1108813","10.1145\/1108792"],"URL":"https:\/\/doi.org\/10.1145\/1108792.1108813","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/1108768.1108813","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2005,9,5]]},"assertion":[{"value":"2005-09-05","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}