{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:07:55Z","timestamp":1761610075002,"version":"build-2065373602"},"reference-count":17,"publisher":"Elsevier BV","issue":"2","license":[{"start":{"date-parts":[[2002,4,1]],"date-time":"2002-04-01T00:00:00Z","timestamp":1017619200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2002,4,1]],"date-time":"2002-04-01T00:00:00Z","timestamp":1017619200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":4137,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2002,4]]},"DOI":"10.1016\/s1571-0661(04)80393-1","type":"journal-article","created":{"date-parts":[[2004,9,28]],"date-time":"2004-09-28T15:29:25Z","timestamp":1096385365000},"page":"2-18","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":14,"title":["VOC"],"prefix":"10.1016","volume":"65","author":[{"given":"Lenore","family":"Zuck","sequence":"first","affiliation":[]},{"given":"Amir","family":"Pnueli","sequence":"additional","affiliation":[]},{"given":"Yi","family":"Fang","sequence":"additional","affiliation":[]},{"given":"Benjamin","family":"Goldberg","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"year":"1988","series-title":"Compilers Principles, Techniques, and Tools","author":"Aho","key":"10.1016\/S1571-0661(04)80393-1_NEWBIB1"},{"key":"10.1016\/S1571-0661(04)80393-1_NEWBIB2","doi-asserted-by":"crossref","unstructured":"R.W. Floyd. Assigning meanings to programs. Proc. Symposia in Applied Mathematics, 19:19\u201332, 1967.","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"10.1016\/S1571-0661(04)80393-1_NEWBIB3","doi-asserted-by":"crossref","unstructured":"Z. Manna, A. Anuchitanukul, N. Bj\u00f8rner, A. Browne, E. Chang, M. Col\u00f3n, L. De Alfaro, H. Devarajan, H. Sipma, and T.E. Uribe. STeP: The Stanford Temporal Prover. Technical Report STAN-CS-TR-94-1518, Dept. of Comp. Sci., Stanford University, Stanford, California, 1994.","DOI":"10.21236\/ADA324036"},{"year":"1997","series-title":"Advanced Compiler Design & Implementation","author":"Muchnick","key":"10.1016\/S1571-0661(04)80393-1_NEWBIB4"},{"key":"10.1016\/S1571-0661(04)80393-1_NEWBIB5","doi-asserted-by":"crossref","unstructured":"G.C. Necula. Proof-carrying code. In Proc. 24th ACM Symp. Princ. of Prog. Lang., pages 106\u2013119, 1997.","DOI":"10.1145\/263699.263712"},{"key":"10.1016\/S1571-0661(04)80393-1_NEWBIB6","doi-asserted-by":"crossref","unstructured":"G. Necula. Translation validation of an optimizing compiler. In Proceedings of the ACM SIGPLAN Conference on Principles of Programming Languages Design and Implementation (PLDI) 2000, pages 83\u201395, 2000.","DOI":"10.1145\/349299.349314"},{"key":"10.1016\/S1571-0661(04)80393-1_NEWBIB7","doi-asserted-by":"crossref","unstructured":"G.C. Necula and P. Lee. The design and implementation of a certifying compilers. In Proceedings of the ACM SIGPLAN Conference on Principles of Programming Languages Design and Implementation (PLDI) 1998, pages 333\u2013344, 1998.","DOI":"10.1145\/277650.277752"},{"key":"10.1016\/S1571-0661(04)80393-1_NEWBIB8","doi-asserted-by":"crossref","unstructured":"A. Pnueli, Y. Rodeh, O. Shtrichman, and M. Siegel. Deciding equality formulas by small-domains instantiations. In In N. Halbwachs and D. Peled, editors, Proc. 11st Intl. Conference on Computer Aided Verification (CAV'99), volume 1633 of Lect. Notes in Comp. Sci., Springer-Verlag, pages 455\u2013469, 1999.","DOI":"10.1007\/3-540-48683-6_39"},{"issue":"2","key":"10.1016\/S1571-0661(04)80393-1_NEWBIB9","doi-asserted-by":"crossref","first-page":"192","DOI":"10.1007\/s100090050027","article-title":"The code validation tool (CVT)-automatic verification of a compilation process","volume":"2","author":"Pnueli","year":"1998","journal-title":"Software Tools for Technology Transfer"},{"key":"10.1016\/S1571-0661(04)80393-1_NEWBIB10","doi-asserted-by":"crossref","unstructured":"A. Pnueli, M. Siegel, and E. Singerman. Translation validation. In In B. Steffen, editor, Proc. 4th Intl. Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'98), volume 1384 of Lect. Notes in Comp. Sci., Springer-Verlag, pages 151\u2013166, 1998.","DOI":"10.1007\/BFb0054170"},{"key":"10.1016\/S1571-0661(04)80393-1_NEWBIB11","unstructured":"A. Pnueli, L. Zuck, and P. Pandya. Translation validation of optimizing compilers by computational induction. Technical report, Courant Institute of Mathematical Sciences, New York University, 2000."},{"key":"10.1016\/S1571-0661(04)80393-1_NEWBIB12","unstructured":"A. Pnueli, L. Zuck, and R. Leviathan. Validation of Optimizing Compilers. Technical report, Computer Science Department, NYU (CIMS\/CS\/NYU.) Available in http:\/\/www.cs.nyu.edu\/validator\/pubs.htm."},{"key":"10.1016\/S1571-0661(04)80393-1_NEWBIB13","unstructured":"M. Rinard and D. Marinov. Credible compilation with pointers. In Proceedings of the Run-Time Result Verification Workshop, Trento, July 2000."},{"key":"10.1016\/S1571-0661(04)80393-1_NEWBIB14","unstructured":"N. Shankar, S. Owre, and J.M. Rushby. The PVS proof checker: A reference manual (draft). Technical report, Comp. Sci. Laboratory, SRI International, Menlo Park, CA, 1993."},{"year":"1999","series-title":"The Mathematica Book","author":"Wolfram","key":"10.1016\/S1571-0661(04)80393-1_NEWBIB15"},{"year":"1991","series-title":"Supercompiler for Parallel and Vector Computers","author":"Zima","key":"10.1016\/S1571-0661(04)80393-1_NEWBIB16"},{"key":"10.1016\/S1571-0661(04)80393-1_NEWBIB17","unstructured":"L. Zuck, A. Pnueli, and B. Goldberg. Translation Validation of Loop Optimizations in Optimizing Compilers. Technical report, CIMS\/CS\/NYU. Available in http:\/\/www.cs.nyu.edu\/validator\/pubs.html."}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104803931?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104803931?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:04:03Z","timestamp":1761609843000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066104803931"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,4]]},"references-count":17,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2002,4]]}},"alternative-id":["S1571066104803931"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(04)80393-1","relation":{},"ISSN":["1571-0661"],"issn-type":[{"type":"print","value":"1571-0661"}],"subject":[],"published":{"date-parts":[[2002,4]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"VOC","name":"articletitle","label":"Article Title"},{"value":"Electronic Notes in Theoretical Computer Science","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/S1571-0661(04)80393-1","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"converted-article","name":"content_type","label":"Content Type"},{"value":"Copyright \u00a9 2002 Published by Elsevier B.V.","name":"copyright","label":"Copyright"}]}}