Formal verification of a C-like memory model and its uses for verifying program transformations

Blazy, Sandrine ; Leroy, Xavier ; et al.

In: Journal of Automated Reasoning Journal of Automated Reasoning, 2008, 41 (1), pp.1-31. ⟨10.1007/s10817-008-9099-0⟩ Journal of Automated Reasoning, Springer Verlag, 2008, 41 (1), pp.1-31. ⟨10.1007/s10817-008-9099-0⟩; (2008)

Online unknown

Wie komme ich dran?

Zugriff:

View record in OpenAIRE (Volltext)

International audience; This article presents the formal verification, using the Coq proof assistant, of a memory model for low-level imperative languages such as C and compiler intermediate languages. Beyond giving semantics to pointer-based programs, this model supports reasoning over transformations of such programs. We show how the properties of the memory model are used to prove semantic preservation for three passes of the Compcert verified compiler

Titel:	Formal verification of a C-like memory model and its uses for verifying program transformations
Autor/in / Beteiligte Person:	Blazy, Sandrine ; Leroy, Xavier ; Programming languages, types, compilation and proofs (GALLIUM) ; Paris-Rocquencourt, Inria ; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria) ; Centre d'études et de recherche en informatique et communications (CEDRIC) ; Ecole Nationale Supérieure d'Informatique pour l'Industrie et l'Entreprise (ENSIIE)-Conservatoire National des Arts et Métiers [CNAM] (CNAM) ; HESAM Université - Communauté d'universités et d'établissements Hautes écoles Sorbonne Arts et métiers université (HESAM)-HESAM Université - Communauté d'universités et d'établissements Hautes écoles Sorbonne Arts et métiers université (HESAM) ; ANR-05-SSIA-0019,CompCert,Certification formelle de compilateurs optimisants pour logiciel embarqué critique(2005)
Link:	View record in OpenAIRE (Volltext) E-Journal im Bestand der UB Hagen? https://inria.hal.science/inria-00289542
Quelle:	Journal of Automated Reasoning Journal of Automated Reasoning, 2008, 41 (1), pp.1-31. ⟨10.1007/s10817-008-9099-0⟩ Journal of Automated Reasoning, Springer Verlag, 2008, 41 (1), pp.1-31. ⟨10.1007/s10817-008-9099-0⟩; (2008)
Veröffentlichung:	HAL CCSD, 2008
Medientyp:	unknown
ISSN:	0168-7433 (print) ; 1573-0670 (print)
Schlagwort:	Theoretical computer science [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL] Computer science Programming language Proof assistant 020207 software engineering 0102 computer and information sciences 02 engineering and technology computer.software_genre 01 natural sciences Imperative programming Computational Theory and Mathematics 010201 computation theory & mathematics Artificial Intelligence Pointer (computer programming) TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS 0202 electrical engineering, electronic engineering, information engineering Compiler Memory model computer Formal verification Software Compiler correctness
Sonstiges:	Nachgewiesen in: OpenAIRE Sprachen: English Language: English Rights: OPEN

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.