A formally verified compiler back-end

Autor: Xavier Leroy
Přispěvatelé: Programming languages, types, compilation and proofs (GALLIUM), Inria Paris-Rocquencourt, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), INRIA Rocquencourt, Institut National de Recherche en Informatique et en Automatique (Inria), ANR-05-SSIA-0019,CompCert,Certification formelle de compilateurs optimisants pour logiciel embarqué critique(2005)
Jazyk: angličtina
Rok vydání: 2009
Předmět:
FOS: Computer and information sciences
Computer Science - Logic in Computer Science
Correctness
Source code
semantic preservation
formal methods
Computer science
media_common.quotation_subject
02 engineering and technology
computer.software_genre
program proof
Artificial Intelligence
020204 information systems
0202 electrical engineering
electronic engineering
information engineering
Compiler verification
Formal verification
Compiled language
computer.programming_language
media_common
Intermediate language
the Coq theorem prover
Computer Science - Programming Languages
[INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL]
Assembly language
Programming language
Proof assistant
[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
020207 software engineering
computer.file_format
Formal methods
Logic in Computer Science (cs.LO)
Computational Theory and Mathematics
compiler transformations and optimizations
TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS
Executable
Compiler
Software_PROGRAMMINGLANGUAGES
Hardware_CONTROLSTRUCTURESANDMICROPROGRAMMING
computer
Software
Programming Languages (cs.PL)
Zdroj: Journal of Automated Reasoning
Journal of Automated Reasoning, Springer Verlag, 2009, 43 (4), pp.363-446. ⟨10.1007/s10817-009-9155-4⟩
Journal of Automated Reasoning, 2009, 43 (4), pp.363-446. ⟨10.1007/s10817-009-9155-4⟩
ISSN: 0168-7433
1573-0670
DOI: 10.1007/s10817-009-9155-4⟩
Popis: International audience; This article describes the development and formal verification (proof of semantic preservation) of a compiler back-end from Cminor (a simple imperative intermediate 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 formal methods applied to the certification of critical software: the verification of the compiler guarantees that the safety properties proved on the source code hold for the executable compiled code as well.
Databáze: OpenAIRE
Externí odkaz: