Formal Verification of a Realistic Compiler.
This paper reports on the development and formal verification (proof of semantic preservation) of Comp Cert, a compiler from Clight (a large subset of the C programming language) to PowerPC assembly code, using the Coq proof assistant both for programming the compiler and for proving its correctness...
| Publicado en: | Communications of the ACM Vol. 52; no. 7; pp. 107 - 116 |
|---|---|
| Autor principal: | |
| Formato: | Artículo |
| Publicado: |
Association for Computing Machinery
Jul2009
|
| Materias: | |
| Acceso en línea: | Ver este registro en EBSCOhost |
| fields | @attributes: recordID: 1 pdfLink: plink: https://search.ebscohost.com/login.aspx?direct=true&db=hlh&AN=43019159&site=ehost-live header: @attributes: shortDbName: hlh uiTerm: 43019159 longDbName: Humanities International Complete uiTag: AN controlInfo: bkinfo: jinfo: jid: 00010782 ACM jtl: Communications of the ACM issn: 00010782 maglogo: N pubinfo: dt: Jul2009 vid: 52 iid: 7 pid: 68 pub: Association for Computing Machinery artinfo: ui: 43019159 10.1145/1538788.1538814 ppf: 107 ppct: 9 formats: tig: atl: Formal Verification of a Realistic Compiler. aug: au: Leroy, Xavier affil: INRIA Paris-Rocquencourt, France. su: Compilers (Computer programs) C (Computer program language) Source code Computer software Systems software PowerPC microprocessors sug: subj: Compilers (Computer programs) C (Computer program language) Source code Computer software Systems software PowerPC microprocessors ab: This paper reports on the development and formal verification (proof of semantic preservation) of Comp Cert, a compiler from Clight (a large subset of the C programming language) to PowerPC assembly code, using the Coq proof assistant both for programming the compiler and for proving its correctness. Such a verified compiler is useful in the context of critical software and its formal verification: the verification of the compiler guarantees that the safety properties proved on the source code hold for the executable compiled code as well. pubtype: Periodical doctype: Article src: R language: English refInfo: copyright: @attributes: flag: Y dt: @attributes: year: 2009 holdings: @attributes: islocal: N |
|---|