{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:46:36Z","timestamp":1772163996042,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":40,"publisher":"ACM","license":[{"start":{"date-parts":[[2009,6,15]],"date-time":"2009-06-15T00:00:00Z","timestamp":1245024000000},"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":[[2009,6,15]]},"DOI":"10.1145\/1542476.1542514","type":"proceedings-article","created":{"date-parts":[[2009,6,16]],"date-time":"2009-06-16T09:34:36Z","timestamp":1245144876000},"page":"338-351","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":36,"title":["An integrated proof language for imperative programs"],"prefix":"10.1145","author":[{"given":"Karen","family":"Zee","sequence":"first","affiliation":[{"name":"Massachusetts Institute of Technology, Cambridge, MA, USA"}]},{"given":"Viktor","family":"Kuncak","sequence":"additional","affiliation":[{"name":"\u00c9cole Polytechnique F\u00e9d\u00e9rale de Lausanne, Lausanne, Switzerland"}]},{"given":"Martin C.","family":"Rinard","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, Cambridge, MA, USA"}]}],"member":"320","published-online":{"date-parts":[[2009,6,15]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-004-0058-x"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-015-9934-4","volume-title":"An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof","author":"Andrews P. B.","year":"2002","unstructured":"P. B. Andrews . An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof . Springer (Kluwer) , 2 nd edition, 2002 . P. B. Andrews. An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof. Springer (Kluwer), 2nd edition, 2002.","edition":"2"},{"key":"e_1_3_2_1_4_1","series-title":"LNCS","volume-title":"ICFEM","author":"Arkoudas K.","year":"2004","unstructured":"K. Arkoudas , K. Zee , V. Kuncak , and M. Rinard . Verifying a file system implementation . In ICFEM , volume 3308 of LNCS , 2004 . K. Arkoudas, K. Zee, V. Kuncak, and M. Rinard. Verifying a file system implementation. In ICFEM, volume 3308 of LNCS, 2004."},{"key":"e_1_3_2_1_5_1","volume-title":"TACAS","author":"Aspinall D.","year":"2000","unstructured":"D. Aspinall . Proof general : A generic tool for proof development . In TACAS , 2000 . D. Aspinall. Proof general: A generic tool for proof development. In TACAS, 2000."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"crossref","unstructured":"R.-J. Back and J. von Wright. Refinement Calculus. Springer-Verlag 1998.  R.-J. Back and J. von Wright. Refinement Calculus. Springer-Verlag 1998.","DOI":"10.1007\/978-1-4612-1674-2"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_12"},{"key":"e_1_3_2_1_8_1","volume-title":"FASE, number 1783 in LNCS","author":"Balser M.","year":"2000","unstructured":"M. Balser , W. Reif , G. Schellhorn , K. Stenzel , and A. Thums . Formal system development with KIV . In FASE, number 1783 in LNCS , 2000 . M. Balser, W. Reif, G. Schellhorn, K. Stenzel, and A. Thums. Formal system development with KIV. In FASE, number 1783 in LNCS, 2000."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5381\/jot.2004.3.6.a2"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development-Coq'Art: The Calculus of Inductive Constructions","author":"Bertot Y.","year":"2004","unstructured":"Y. Bertot and P. Cast\u00e9ran . Interactive Theorem Proving and Program Development-Coq'Art: The Calculus of Inductive Constructions . Springer , 2004 . Y. Bertot and P. Cast\u00e9ran. Interactive Theorem Proving and Program Development-Coq'Art: The Calculus of Inductive Constructions. Springer, 2004."},{"key":"e_1_3_2_1_11_1","first-page":"83","volume-title":"Machine Intelligence","author":"Boyer R. S.","year":"1988","unstructured":"R. S. Boyer and J. S. Moore . Integrating decision procedures into heuristic theorem provers: A case study of linear arithmetic . In Machine Intelligence , volume 11 , pages 83 -- 124 . OUP , 1988 . R. S. Boyer and J. S. Moore. Integrating decision procedures into heuristic theorem provers: A case study of linear arithmetic. In Machine Intelligence, volume 11, pages 83--124. OUP, 1988."},{"key":"e_1_3_2_1_12_1","volume-title":"VSTTE","author":"Chalin P.","year":"2005","unstructured":"P. Chalin , C. Hurlin , and J. Kiniry . Integrating static checking and interactive verification: Supporting multiple theories and provers in verification . In VSTTE , 2005 . P. Chalin, C. Hurlin, and J. Kiniry. Integrating static checking and interactive verification: Supporting multiple theories and provers in verification. In VSTTE, 2005."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90005-3"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73595-3_13"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679680200446X"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512558"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503291"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360220"},{"key":"e_1_3_2_1_21_1","volume-title":"http:\/\/www.cis.upenn.edu\/~jean\/gbooks\/logic.html, revised on-line edition","author":"Gallier J.","year":"2003","unstructured":"J. Gallier . Logic for Computer Science . http:\/\/www.cis.upenn.edu\/~jean\/gbooks\/logic.html, revised on-line edition , 2003 . J. Gallier. Logic for Computer Science. http:\/\/www.cis.upenn.edu\/~jean\/gbooks\/logic.html, revised on-line edition, 2003."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73595-3_12"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30124-0_15"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2006.125"},{"key":"e_1_3_2_1_26_1","volume-title":"Second International Workshop on Automated Verification of Infinite-State Systems (AVIS'03)","author":"Kuncak V.","year":"2003","unstructured":"V. Kuncak and K. R. M. Leino . In-place refinement for effect checking . In Second International Workshop on Automated Verification of Infinite-State Systems (AVIS'03) , Warsaw, Poland , April 2003 . V. Kuncak and K. R. M. Leino. In-place refinement for effect checking. In Second International Workshop on Automated Verification of Infinite-State Systems (AVIS'03), Warsaw, Poland, April 2003."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-006-9042-1"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/1760267.1760301"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73595-3_15"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1052898.1052913"},{"key":"e_1_3_2_1_32_1","unstructured":"K. R. M. Leino. This is Boogie 2. http:\/\/research.microsoft.com\/leino\/papers\/krml178.pdf June 2008. (working draft).  K. R. M. Leino. This is Boogie 2. http:\/\/research.microsoft.com\/leino\/papers\/krml178.pdf June 2008. (working draft)."},{"key":"e_1_3_2_1_33_1","first-page":"70","volume-title":"ESCoR: Empir. Successful Comp. Reasoning","author":"Meng J.","year":"2006","unstructured":"J. Meng and L. C. Paulson . Translating higher-order problems to first-order clauses . In ESCoR: Empir. Successful Comp. Reasoning , pages 70 -- 80 , 2006 . J. Meng and L. C. Paulson. Translating higher-order problems to first-order clauses. In ESCoR: Empir. Successful Comp. Reasoning, pages 70--80, 2006."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411237"},{"key":"e_1_3_2_1_35_1","series-title":"LNCS","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"Nipkow T.","year":"2002","unstructured":"T. Nipkow , L. C. Paulson , and M. Wenzel . Isabelle\/HOL: A Proof Assistant for Higher-Order Logic , volume 2283 of LNCS . Springer-Verlag , 2002 . T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle\/HOL: A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer-Verlag, 2002."},{"key":"e_1_3_2_1_36_1","volume-title":"Programming in Martin-Loef's Type Theory: An Introduction","author":"Nordstroem B.","year":"1990","unstructured":"B. Nordstroem , K. Petersson , and J. Smith . Programming in Martin-Loef's Type Theory: An Introduction . Oxford University Press , 1990 . B. Nordstroem, K. Petersson, and J. Smith. Programming in Martin-Loef's Type Theory: An Introduction. Oxford University Press, 1990."},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.5555\/648230.752639"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.5555\/34057"},{"key":"e_1_3_2_1_39_1","volume-title":"Department of Computer Science","author":"Ranise S.","year":"2006","unstructured":"S. Ranise and C. Tinelli . The SMT-LIB Standard: Version 1.2. Technical report , Department of Computer Science , The University of Iowa , 2006 . Available at www.SMT-LIB.org. S. Ranise and C. Tinelli. The SMT-LIB Standard: Version 1.2. Technical report, Department of Computer Science, The University of Iowa, 2006. Available at www.SMT-LIB.org."},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1006218513245"},{"issue":"2","key":"e_1_3_2_1_41_1","first-page":"111","volume":"15","author":"Schulz S.","year":"2002","unstructured":"S. Schulz . E -- A Brainiac Theorem Prover . Journal of AI Communications , 15 ( 2\/3 ): 111 -- 126 , 2002 . S. Schulz. E -- A Brainiac Theorem Prover. Journal of AI Communications, 15(2\/3):111--126, 2002.","journal-title":"Journal of AI Communications"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.5555\/778522.778536"},{"key":"e_1_3_2_1_44_1","volume-title":"TU Munchen","author":"Wenzel M.","year":"2002","unstructured":"M. Wenzel . Isabelle\/Isar -- a versatile environment for human-readable formal proof documents. PhD thesis , TU Munchen , 2002 . M. Wenzel. Isabelle\/Isar -- a versatile environment for human-readable formal proof documents. PhD thesis, TU Munchen, 2002."},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796806006216"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375624"}],"event":{"name":"PLDI '09: ACM SIGPLAN Conference on Programming Language Design and Implementation","location":"Dublin Ireland","acronym":"PLDI '09","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","ACM Association for Computing Machinery"]},"container-title":["Proceedings of the 30th ACM SIGPLAN Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1542476.1542514","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1542476.1542514","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T09:29:49Z","timestamp":1750238989000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1542476.1542514"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,6,15]]},"references-count":40,"alternative-id":["10.1145\/1542476.1542514","10.1145\/1542476"],"URL":"https:\/\/doi.org\/10.1145\/1542476.1542514","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/1543135.1542514","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2009,6,15]]},"assertion":[{"value":"2009-06-15","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}