<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE article PUBLIC "-//TaxonX//DTD Taxonomic Treatment Publishing DTD v0 20100105//EN" "../../nlm/tax-treatment-NS0.dtd">
<article xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:tp="http://www.plazi.org/taxpub" article-type="research-article" dtd-version="3.0" xml:lang="en">
  <front>
    <journal-meta>
      <journal-id journal-id-type="publisher-id">109</journal-id>
      <journal-id journal-id-type="index">urn:lsid:arphahub.com:pub:3dc5f44e-8666-58db-bc76-a455210e8891</journal-id>
      <journal-title-group>
        <journal-title xml:lang="en">JUCS - Journal of Universal Computer Science</journal-title>
        <abbrev-journal-title xml:lang="en">jucs</abbrev-journal-title>
      </journal-title-group>
      <issn pub-type="ppub">0948-695X</issn>
      <issn pub-type="epub">0948-6968</issn>
      <publisher>
        <publisher-name>Journal of Universal Computer Science</publisher-name>
      </publisher>
    </journal-meta>
    <article-meta>
      <article-id pub-id-type="doi">10.3217/jucs-009-03-0223</article-id>
      <article-id pub-id-type="publisher-id">27937</article-id>
      <article-categories>
        <subj-group subj-group-type="heading">
          <subject>Research Article</subject>
        </subj-group>
        <subj-group subj-group-type="scientific_subject">
          <subject>D.2.4 - Software/Program Verification</subject>
          <subject>D.3.4 - Processors</subject>
          <subject>I.6.4 - Model Validation and Analysis</subject>
        </subj-group>
      </article-categories>
      <title-group>
        <article-title>VOC: A Methodology for the Translation Validation of OptimizingCompilers</article-title>
      </title-group>
      <contrib-group content-type="authors">
        <contrib contrib-type="author" corresp="yes">
          <name name-style="western">
            <surname>Zuck</surname>
            <given-names>Lenore</given-names>
          </name>
          <email xlink:type="simple">zuck@cs.nyu.edu</email>
          <xref ref-type="aff" rid="A1">1</xref>
        </contrib>
        <contrib contrib-type="author" corresp="no">
          <name name-style="western">
            <surname>Pnueli</surname>
            <given-names>Amir</given-names>
          </name>
          <xref ref-type="aff" rid="A2">2</xref>
        </contrib>
        <contrib contrib-type="author" corresp="no">
          <name name-style="western">
            <surname>Fang</surname>
            <given-names>Yi</given-names>
          </name>
          <xref ref-type="aff" rid="A3">3</xref>
        </contrib>
        <contrib contrib-type="author" corresp="no">
          <name name-style="western">
            <surname>Goldberg</surname>
            <given-names>Benjamin</given-names>
          </name>
          <xref ref-type="aff" rid="A3">3</xref>
        </contrib>
      </contrib-group>
      <aff id="A1">
        <label>1</label>
        <addr-line content-type="verbatim">New York University, , United States of America</addr-line>
        <institution>New York University</institution>
        <country>United States of America</country>
      </aff>
      <aff id="A2">
        <label>2</label>
        <addr-line content-type="verbatim">Weizmann Institute of Science, Israel and New York University, New York, United States of America</addr-line>
        <institution>Weizmann Institute of Science, Israel and New York University</institution>
        <addr-line content-type="city">New York</addr-line>
        <country>United States of America</country>
      </aff>
      <aff id="A3">
        <label>3</label>
        <addr-line content-type="verbatim">New York University, New York, United States of America</addr-line>
        <institution>New York University</institution>
        <addr-line content-type="city">New York</addr-line>
        <country>United States of America</country>
      </aff>
      <author-notes>
        <fn fn-type="corresp">
          <p>Corresponding author: Lenore Zuck (<email xlink:type="simple">zuck@cs.nyu.edu</email>).</p>
        </fn>
        <fn fn-type="edited-by">
          <p>Academic editor: </p>
        </fn>
      </author-notes>
      <pub-date pub-type="collection">
        <year>2003</year>
      </pub-date>
      <pub-date pub-type="epub">
        <day>28</day>
        <month>03</month>
        <year>2003</year>
      </pub-date>
      <volume>9</volume>
      <issue>3</issue>
      <fpage>223</fpage>
      <lpage>247</lpage>
      <uri content-type="arpha" xlink:href="http://openbiodiv.net/5D25EAB5-AECC-5E5C-88E5-E037A24BFE77">5D25EAB5-AECC-5E5C-88E5-E037A24BFE77</uri>
      <uri content-type="zenodo_dep_id" xlink:href="https://zenodo.org/record/6996288">6996288</uri>
      <permissions>
        <copyright-statement>Lenore Zuck, Amir Pnueli, Yi Fang, Benjamin Goldberg</copyright-statement>
        <license license-type="creative-commons-attribution" xlink:href="" xlink:type="simple">
          <license-p>This article is freely available under the J.UCS Open Content License.</license-p>
        </license>
      </permissions>
      <abstract>
        <label>Abstract</label>
        <p>There is a growing awareness, both in industry and academia, of the crucial role of formally verifying the translation from high-level source-code into low-level object code that is typically performed by an optimizing compiler. Formally verifying an optimizing compiler, as one would verify any other large program, is not feasible due to its size, ongoing evolution and modification, and, possibly, proprietary considerations. Translation validation is a novel approach that offers an alternative to the verification of translators in general and compilers in particular: Rather than verifying the compiler itself, one constructs a validation tool which, after every run of the compiler, formally confirms that the target code produced in the run is a correct translation of the source program. The paper presents voc, a methodology for the translation validation of optimizing compilers. We distinguish between structure preserving optimizations, for which we establish a simulation relation between the source and target code based on computational induction, and structure modifying optimizations, for which we develop specialized permutation rules. The paper also describes voc-64 - a prototype translation validator tool that automatically produces verification conditions for the global optimizations of the SGI Pro-64 compiler.</p>
      </abstract>
    </article-meta>
  </front>
</article>
