<?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-0191</article-id>
      <article-id pub-id-type="publisher-id">27936</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>F.3.1 - Specifying and Verifying and Reasoning about Programs</subject>
          <subject>F.4.2 - Grammars and Other Rewriting Systems</subject>
        </subj-group>
      </article-categories>
      <title-group>
        <article-title>Using Program Checking to Ensure the Correctness of Compiler Implementations</article-title>
      </title-group>
      <contrib-group content-type="authors">
        <contrib contrib-type="author" corresp="yes">
          <name name-style="western">
            <surname>Glesner</surname>
            <given-names>Sabine</given-names>
          </name>
          <email xlink:type="simple">glesner@ipd.info.uni-karlsruhe.de</email>
          <xref ref-type="aff" rid="A1">1</xref>
        </contrib>
      </contrib-group>
      <aff id="A1">
        <label>1</label>
        <addr-line content-type="verbatim">Institute for Program Structures and Data Organization University of Karlsruhe, Karlsruhe, Germany</addr-line>
        <institution>Institute for Program Structures and Data Organization University of Karlsruhe</institution>
        <addr-line content-type="city">Karlsruhe</addr-line>
        <country>Germany</country>
      </aff>
      <author-notes>
        <fn fn-type="corresp">
          <p>Corresponding author: Sabine Glesner (<email xlink:type="simple">glesner@ipd.info.uni-karlsruhe.de</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>191</fpage>
      <lpage>222</lpage>
      <uri content-type="arpha" xlink:href="http://openbiodiv.net/8CD196EF-C8CC-59E0-BDB0-418D06020885">8CD196EF-C8CC-59E0-BDB0-418D06020885</uri>
      <uri content-type="zenodo_dep_id" xlink:href="https://zenodo.org/record/6996286">6996286</uri>
      <permissions>
        <copyright-statement>Sabine Glesner</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>We evaluate the use of program checking to ensure the correctness of compiler implementations. Our contributions in this paper are threefold: Firstly, we extend the classical notion of black-box program checking to program checking with certificates. Our checking approach with certificates relies on the observation that the correctness of solutions of NP-complete problems can be checked in polynomial time whereas their computation itself is believed to be much harder. Our second contribution is the application of program checking with certificates to optimizing compiler backends, in particular code generators, thus answering the open question of how program checking for such compiler backends can be achieved. In particular, we state a checking algorithm for code generation based on bottom-up rewrite systems from static single assignment representations. We have implemented this algorithm in a checker for a code generator used in an industrial project. Our last contribution in this paper is an integrated view on all compiler passes, in particular a comparison between frontend and backend phases, with respect to the applicable methods of program checking.</p>
      </abstract>
    </article-meta>
  </front>
</article>
