Formal certification of a compiler back-end or : Programming a compiler with a proof assistant

LEROY, Xavier

In: Conference record of POPL® 2006: The 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages®, January 11-13, 2006, Charleston, South Carolina, USAACM SIGPLAN notices 41(1):42-54

Konferenz - print, 35 ref

Wie komme ich dran?

This paper reports on the development and formal certification (proof of semantic preservation) of a compiler from Cminor (a C-like imperative language) to PowerPC assembly code, using the Coq proof assistant both for programming the compiler and for proving its correctness. Such a certified compiler is useful in the context of formal methods applied to the certification of critical software: the certification of the compiler guarantees that the safety properties proved on the source code bold for the executable compiled code as well.

Titel:	Formal certification of a compiler back-end or : Programming a compiler with a proof assistant
Autor/in / Beteiligte Person:	LEROY, Xavier
Link:	View record from PASCAL Archive
Quelle:	Conference record of POPL® 2006: The 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages®, January 11-13, 2006, Charleston, South Carolina, USAACM SIGPLAN notices 41(1):42-54
Veröffentlichung:	Broadway, NY: ACM, 2006
Medientyp:	Konferenz
Umfang:	print, 35 ref
ISSN:	1523-2867 (print)
Schlagwort:	Computer science Informatique Sciences exactes et technologie Exact sciences and technology Sciences appliquees Applied sciences Informatique; automatique theorique; systemes Computer science; control theory; systems Informatique théorique Theoretical computing Théorie des langages et analyse syntaxique Language theory and syntactical analysis Logiciel Software Langages de programmation Programming languages Génie logiciel Software engineering Compilateur Compiler Compilador Compilation Compilación Langage impératif Imperative language Lenguaje imperativo Langage programmation Programming language Lenguaje programación Logiciel à sécurité critique Safety-critical software Optimisation compilateur Compiler optimization Optimización compiladora Preuve programme Program proof Prueba programa Sémantique formelle Formal semantics Semántica formal Vérification formelle Formal verification Vérification programme Program verification Verificación programa Certification formelle Coq theorem prover Préservation sémantique Transformation compilateur Languages Reliability Security Verification. Certified compilation compiler transformations and optimizations program proof semantic preservation the Coq theorem prover
Sonstiges:	Nachgewiesen in: PASCAL Archive Sprachen: English Original Material: INIST-CNRS Document Type: Conference Paper File Description: text Language: English Author Affiliations: INRIA Rocquencourt, France Rights: Copyright 2006 INIST-CNRS ; CC BY 4.0 ; Sauf mention contraire ci-dessus, le contenu de cette notice bibliographique peut être utilisé dans le cadre d’une licence CC BY 4.0 Inist-CNRS / Unless otherwise stated above, the content of this bibliographic record may be used under a CC BY 4.0 licence by Inist-CNRS / A menos que se haya señalado antes, el contenido de este registro bibliográfico puede ser utilizado al amparo de una licencia CC BY 4.0 Inist-CNRS Notes: Computer science; theoretical automation; systems

Klicken Sie ein Format an und speichern Sie dann die Daten oder geben Sie eine Empfänger-Adresse ein und lassen Sie sich per Email zusenden.

BibTeX Citavi, JabRef, u.a.
(Literaturverwaltung)

PDF kein Volltext!
(Merkzettel, Notizen)

RIS Endnote, Citavi u.a.
(Literaturverwaltung)

MODS
(XML zur Weiterverarbeitung)

oder

Wählen Sie das für Sie passende Zitationsformat und kopieren Sie es dann in die Zwischenablage, lassen es sich per Mail zusenden oder speichern es als PDF-Datei.

Gewünschter Zitations-Stil:

oder

Bitte prüfen Sie, ob die Zitation formal korrekt ist, bevor Sie sie in einer Arbeit verwenden. Benutzen Sie gegebenenfalls den "Exportieren"-Dialog, wenn Sie ein Literaturverwaltungsprogramm verwenden und die Zitat-Angaben selbst formatieren wollen.