Loading…
Certifying compilers using higher-order theorem provers as certificate checkers
Correct software requires compilers to work correctly. Especially code generation can be an error prone task, since it potentially uses sophisticated algorithms to produce efficient code. In this paper we present an approach to guarantee the correctness of compiler transformations with respect to a...
Saved in:
| Published in: | Formal methods in system design 2011-02, Vol.38 (1), p.33-61 |
|---|---|
| Main Authors: | , |
| Format: | Article |
| Language: | English |
| Subjects: | |
| Citations: | Items that this one cites Items that cite this one |
| Online Access: | Get full text |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| cited_by | cdi_FETCH-LOGICAL-c321t-ba9bbf2e18478ce8540403b50bde3cf6978513d0fc743c7cbf15b45791ac19473 |
|---|---|
| cites | cdi_FETCH-LOGICAL-c321t-ba9bbf2e18478ce8540403b50bde3cf6978513d0fc743c7cbf15b45791ac19473 |
| container_end_page | 61 |
| container_issue | 1 |
| container_start_page | 33 |
| container_title | Formal methods in system design |
| container_volume | 38 |
| creator | Blech, Jan Olaf Grégoire, Benjamin |
| description | Correct software requires compilers to work correctly. Especially code generation can be an error prone task, since it potentially uses sophisticated algorithms to produce efficient code.
In this paper we present an approach to guarantee the correctness of compiler transformations with respect to a formal notion of correctness. We certify the results of each compilation run. With the help of a compiler generated certificate and a certificate checker, we verify the results of each compilation run automatically. Thereby we ensure the correctness of the compilation run without having to look at concrete compilation algorithms.
We use higher-order theorem provers to check the certificates and to formally define syntax, and semantics of the involved languages as well as a criterion under which we regard a compilation as correct. The use of higher-order theorem provers ensures a small and well understood trusted computing base. The task of efficient certificate checking is especially crucial for the acceptance of certifying compilation. We present methods to facilitate this task, most notably by using computational reflection: We present small—in an executable way specified—evaluators that solve certain properties appearing in our certificates and are used to speed up certain subtasks in the checking process.
We discuss an implemented prototype performing code generation. Using Coq and Isabelle/HOL as certificate checkers we highlight typical challenges and their solutions |
| doi_str_mv | 10.1007/s10703-010-0108-7 |
| format | article |
| fullrecord | <record><control><sourceid>proquest_cross</sourceid><recordid>TN_cdi_proquest_miscellaneous_1671335539</recordid><sourceformat>XML</sourceformat><sourcesystem>PC</sourcesystem><sourcerecordid>1671335539</sourcerecordid><originalsourceid>FETCH-LOGICAL-c321t-ba9bbf2e18478ce8540403b50bde3cf6978513d0fc743c7cbf15b45791ac19473</originalsourceid><addsrcrecordid>eNp9kE1PwzAMhiMEEmPwA7j1yCVgN02THtHElzRpFzhHaeauHf0iaZH272kpZw6WZet5X9kvY7cI9wigHgKCAsEBYS7N1RlboVQx1wjxOVtBFkueaZlesqsQjgCgMRUrttuQH6riVLWHyHVNX9XkQzSGeS6rQ0med35PPhpK6jw1Ue-77xmxIXK_0srZgSJXkvuc9tfsorB1oJu_vmYfz0_vm1e-3b28bR633IkYB57bLM-LmFAnSjvSMoEERC4h35NwRZopLVHsoXAqEU65vECZJ1JlaB1miRJrdrf4Tvd8jRQG01TBUV3blroxGEwVCiGlyCYUF9T5LgRPhel91Vh_MghmDs8s4ZkpuLm0me3jRRMmtj2QN8du9O300T-iH8HKcqM</addsrcrecordid><sourcetype>Aggregation Database</sourcetype><iscdi>true</iscdi><recordtype>article</recordtype><pqid>1671335539</pqid></control><display><type>article</type><title>Certifying compilers using higher-order theorem provers as certificate checkers</title><source>Springer Nature</source><creator>Blech, Jan Olaf ; Grégoire, Benjamin</creator><creatorcontrib>Blech, Jan Olaf ; Grégoire, Benjamin</creatorcontrib><description>Correct software requires compilers to work correctly. Especially code generation can be an error prone task, since it potentially uses sophisticated algorithms to produce efficient code.
In this paper we present an approach to guarantee the correctness of compiler transformations with respect to a formal notion of correctness. We certify the results of each compilation run. With the help of a compiler generated certificate and a certificate checker, we verify the results of each compilation run automatically. Thereby we ensure the correctness of the compilation run without having to look at concrete compilation algorithms.
We use higher-order theorem provers to check the certificates and to formally define syntax, and semantics of the involved languages as well as a criterion under which we regard a compilation as correct. The use of higher-order theorem provers ensures a small and well understood trusted computing base. The task of efficient certificate checking is especially crucial for the acceptance of certifying compilation. We present methods to facilitate this task, most notably by using computational reflection: We present small—in an executable way specified—evaluators that solve certain properties appearing in our certificates and are used to speed up certain subtasks in the checking process.
We discuss an implemented prototype performing code generation. Using Coq and Isabelle/HOL as certificate checkers we highlight typical challenges and their solutions</description><identifier>ISSN: 0925-9856</identifier><identifier>EISSN: 1572-8102</identifier><identifier>DOI: 10.1007/s10703-010-0108-7</identifier><language>eng</language><publisher>Boston: Springer US</publisher><subject>CAE) and Design ; Checkers ; Circuits and Systems ; Compilers ; Computer programs ; Computer-Aided Engineering (CAD ; Electrical Engineering ; Engineering ; Formal method ; Software ; Software Engineering/Programming and Operating Systems ; Systems design ; Tasks ; Theorem proving</subject><ispartof>Formal methods in system design, 2011-02, Vol.38 (1), p.33-61</ispartof><rights>Springer Science+Business Media, LLC 2010</rights><lds50>peer_reviewed</lds50><woscitedreferencessubscribed>false</woscitedreferencessubscribed><citedby>FETCH-LOGICAL-c321t-ba9bbf2e18478ce8540403b50bde3cf6978513d0fc743c7cbf15b45791ac19473</citedby><cites>FETCH-LOGICAL-c321t-ba9bbf2e18478ce8540403b50bde3cf6978513d0fc743c7cbf15b45791ac19473</cites></display><links><openurl>$$Topenurl_article</openurl><openurlfulltext>$$Topenurlfull_article</openurlfulltext><thumbnail>$$Tsyndetics_thumb_exl</thumbnail><link.rule.ids>314,776,780,27903,27904</link.rule.ids></links><search><creatorcontrib>Blech, Jan Olaf</creatorcontrib><creatorcontrib>Grégoire, Benjamin</creatorcontrib><title>Certifying compilers using higher-order theorem provers as certificate checkers</title><title>Formal methods in system design</title><addtitle>Form Methods Syst Des</addtitle><description>Correct software requires compilers to work correctly. Especially code generation can be an error prone task, since it potentially uses sophisticated algorithms to produce efficient code.
In this paper we present an approach to guarantee the correctness of compiler transformations with respect to a formal notion of correctness. We certify the results of each compilation run. With the help of a compiler generated certificate and a certificate checker, we verify the results of each compilation run automatically. Thereby we ensure the correctness of the compilation run without having to look at concrete compilation algorithms.
We use higher-order theorem provers to check the certificates and to formally define syntax, and semantics of the involved languages as well as a criterion under which we regard a compilation as correct. The use of higher-order theorem provers ensures a small and well understood trusted computing base. The task of efficient certificate checking is especially crucial for the acceptance of certifying compilation. We present methods to facilitate this task, most notably by using computational reflection: We present small—in an executable way specified—evaluators that solve certain properties appearing in our certificates and are used to speed up certain subtasks in the checking process.
We discuss an implemented prototype performing code generation. Using Coq and Isabelle/HOL as certificate checkers we highlight typical challenges and their solutions</description><subject>CAE) and Design</subject><subject>Checkers</subject><subject>Circuits and Systems</subject><subject>Compilers</subject><subject>Computer programs</subject><subject>Computer-Aided Engineering (CAD</subject><subject>Electrical Engineering</subject><subject>Engineering</subject><subject>Formal method</subject><subject>Software</subject><subject>Software Engineering/Programming and Operating Systems</subject><subject>Systems design</subject><subject>Tasks</subject><subject>Theorem proving</subject><issn>0925-9856</issn><issn>1572-8102</issn><fulltext>true</fulltext><rsrctype>article</rsrctype><creationdate>2011</creationdate><recordtype>article</recordtype><recordid>eNp9kE1PwzAMhiMEEmPwA7j1yCVgN02THtHElzRpFzhHaeauHf0iaZH272kpZw6WZet5X9kvY7cI9wigHgKCAsEBYS7N1RlboVQx1wjxOVtBFkueaZlesqsQjgCgMRUrttuQH6riVLWHyHVNX9XkQzSGeS6rQ0med35PPhpK6jw1Ue-77xmxIXK_0srZgSJXkvuc9tfsorB1oJu_vmYfz0_vm1e-3b28bR633IkYB57bLM-LmFAnSjvSMoEERC4h35NwRZopLVHsoXAqEU65vECZJ1JlaB1miRJrdrf4Tvd8jRQG01TBUV3blroxGEwVCiGlyCYUF9T5LgRPhel91Vh_MghmDs8s4ZkpuLm0me3jRRMmtj2QN8du9O300T-iH8HKcqM</recordid><startdate>20110201</startdate><enddate>20110201</enddate><creator>Blech, Jan Olaf</creator><creator>Grégoire, Benjamin</creator><general>Springer US</general><scope>AAYXX</scope><scope>CITATION</scope><scope>7SP</scope><scope>8FD</scope><scope>L7M</scope></search><sort><creationdate>20110201</creationdate><title>Certifying compilers using higher-order theorem provers as certificate checkers</title><author>Blech, Jan Olaf ; Grégoire, Benjamin</author></sort><facets><frbrtype>5</frbrtype><frbrgroupid>cdi_FETCH-LOGICAL-c321t-ba9bbf2e18478ce8540403b50bde3cf6978513d0fc743c7cbf15b45791ac19473</frbrgroupid><rsrctype>articles</rsrctype><prefilter>articles</prefilter><language>eng</language><creationdate>2011</creationdate><topic>CAE) and Design</topic><topic>Checkers</topic><topic>Circuits and Systems</topic><topic>Compilers</topic><topic>Computer programs</topic><topic>Computer-Aided Engineering (CAD</topic><topic>Electrical Engineering</topic><topic>Engineering</topic><topic>Formal method</topic><topic>Software</topic><topic>Software Engineering/Programming and Operating Systems</topic><topic>Systems design</topic><topic>Tasks</topic><topic>Theorem proving</topic><toplevel>peer_reviewed</toplevel><toplevel>online_resources</toplevel><creatorcontrib>Blech, Jan Olaf</creatorcontrib><creatorcontrib>Grégoire, Benjamin</creatorcontrib><collection>CrossRef</collection><collection>Electronics & Communications Abstracts</collection><collection>Technology Research Database</collection><collection>Advanced Technologies Database with Aerospace</collection><jtitle>Formal methods in system design</jtitle></facets><delivery><delcategory>Remote Search Resource</delcategory><fulltext>fulltext</fulltext></delivery><addata><au>Blech, Jan Olaf</au><au>Grégoire, Benjamin</au><format>journal</format><genre>article</genre><ristype>JOUR</ristype><atitle>Certifying compilers using higher-order theorem provers as certificate checkers</atitle><jtitle>Formal methods in system design</jtitle><stitle>Form Methods Syst Des</stitle><date>2011-02-01</date><risdate>2011</risdate><volume>38</volume><issue>1</issue><spage>33</spage><epage>61</epage><pages>33-61</pages><issn>0925-9856</issn><eissn>1572-8102</eissn><abstract>Correct software requires compilers to work correctly. Especially code generation can be an error prone task, since it potentially uses sophisticated algorithms to produce efficient code.
In this paper we present an approach to guarantee the correctness of compiler transformations with respect to a formal notion of correctness. We certify the results of each compilation run. With the help of a compiler generated certificate and a certificate checker, we verify the results of each compilation run automatically. Thereby we ensure the correctness of the compilation run without having to look at concrete compilation algorithms.
We use higher-order theorem provers to check the certificates and to formally define syntax, and semantics of the involved languages as well as a criterion under which we regard a compilation as correct. The use of higher-order theorem provers ensures a small and well understood trusted computing base. The task of efficient certificate checking is especially crucial for the acceptance of certifying compilation. We present methods to facilitate this task, most notably by using computational reflection: We present small—in an executable way specified—evaluators that solve certain properties appearing in our certificates and are used to speed up certain subtasks in the checking process.
We discuss an implemented prototype performing code generation. Using Coq and Isabelle/HOL as certificate checkers we highlight typical challenges and their solutions</abstract><cop>Boston</cop><pub>Springer US</pub><doi>10.1007/s10703-010-0108-7</doi><tpages>29</tpages></addata></record> |
| fulltext | fulltext |
| identifier | ISSN: 0925-9856 |
| ispartof | Formal methods in system design, 2011-02, Vol.38 (1), p.33-61 |
| issn | 0925-9856 1572-8102 |
| language | eng |
| recordid | cdi_proquest_miscellaneous_1671335539 |
| source | Springer Nature |
| subjects | CAE) and Design Checkers Circuits and Systems Compilers Computer programs Computer-Aided Engineering (CAD Electrical Engineering Engineering Formal method Software Software Engineering/Programming and Operating Systems Systems design Tasks Theorem proving |
| title | Certifying compilers using higher-order theorem provers as certificate checkers |
| url | http://sfxeu10.hosted.exlibrisgroup.com/loughborough?ctx_ver=Z39.88-2004&ctx_enc=info:ofi/enc:UTF-8&ctx_tim=2025-01-25T23%3A43%3A25IST&url_ver=Z39.88-2004&url_ctx_fmt=infofi/fmt:kev:mtx:ctx&rfr_id=info:sid/primo.exlibrisgroup.com:primo3-Article-proquest_cross&rft_val_fmt=info:ofi/fmt:kev:mtx:journal&rft.genre=article&rft.atitle=Certifying%20compilers%20using%20higher-order%20theorem%20provers%20as%20certificate%20checkers&rft.jtitle=Formal%20methods%20in%20system%20design&rft.au=Blech,%20Jan%20Olaf&rft.date=2011-02-01&rft.volume=38&rft.issue=1&rft.spage=33&rft.epage=61&rft.pages=33-61&rft.issn=0925-9856&rft.eissn=1572-8102&rft_id=info:doi/10.1007/s10703-010-0108-7&rft_dat=%3Cproquest_cross%3E1671335539%3C/proquest_cross%3E%3Cgrp_id%3Ecdi_FETCH-LOGICAL-c321t-ba9bbf2e18478ce8540403b50bde3cf6978513d0fc743c7cbf15b45791ac19473%3C/grp_id%3E%3Coa%3E%3C/oa%3E%3Curl%3E%3C/url%3E&rft_id=info:oai/&rft_pqid=1671335539&rft_id=info:pmid/&rfr_iscdi=true |