Tilting at windmills with Coq: formal verification of a compilation algorithm for parallel moves
| Autor: | Bernard Serpette, Laurence Rideau, Xavier Leroy |
|---|---|
| Přispěvatelé: | Mathematical, Reasoning and Software (MARELLE), Inria Sophia Antipolis - Méditerranée (CRISAM), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Active objects, semantics, Internet and security (OASIS), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-COMmunications, Réseaux, systèmes Embarqués et Distribués (Laboratoire I3S - COMRED), Laboratoire d'Informatique, Signaux, et Systèmes de Sophia Antipolis (I3S), Université Nice Sophia Antipolis (... - 2019) (UNS), COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UCA)-Université Nice Sophia Antipolis (... - 2019) (UNS), COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UCA)-Laboratoire d'Informatique, Signaux, et Systèmes de Sophia Antipolis (I3S), COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UCA), Programming languages, types, compilation and proofs (GALLIUM), Inria Paris-Rocquencourt, ANR-05-SSIA-0019,CompCert,Certification formelle de compilateurs optimisants pour logiciel embarqué critique(2005), Université Nice Sophia Antipolis (1965 - 2019) (UNS), COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UCA)-Université Nice Sophia Antipolis (1965 - 2019) (UNS) |
| Jazyk: | angličtina |
| Rok vydání: | 2008 |
| Předmět: |
Sequence
Correctness Theoretical computer science [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL] Programming language Computer science Correctness proofs [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] 020207 software engineering 02 engineering and technology computer.software_genre Computational Theory and Mathematics Artificial Intelligence 0202 electrical engineering electronic engineering information engineering Computer Science::Programming Languages 020201 artificial intelligence & image processing Compiler Formal verification computer Algorithm Software Compiler correctness |
| Zdroj: | Journal of Automated Reasoning Journal of Automated Reasoning, Springer Verlag, 2008, 40 (4), pp.307-326. ⟨10.1007/s10817-007-9096-8⟩ Journal of Automated Reasoning, 2008, 40 (4), pp.307-326. ⟨10.1007/s10817-007-9096-8⟩ |
| ISSN: | 0168-7433 1573-0670 |
| Popis: | International audience; This article describes the formal verification of a compilation algorithm that transforms parallel moves (parallel assignments between variables) into a semantically-equivalent sequence of elementary moves. Two different specifications of the algorithm are given: an inductive specification and a functional one, each with its correctness proofs. A functional program can then be extracted and integrated in the Compcert verified compiler. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full text from SpringerLink