From 86fa4cc62f34f8fda7ea324c692101a97b4b8166 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Mon, 6 Dec 2021 15:30:13 +0100 Subject: update info on authors/papers --- README.md | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) (limited to 'README.md') diff --git a/README.md b/README.md index 3990048e..88e37055 100644 --- a/README.md +++ b/README.md @@ -20,6 +20,7 @@ the [user's manual](https://compcert.org/man/). This is a special version with additions from Verimag and Kalray : * A backend for the KVX processor: see [`README_Kalray.md`](README_Kalray.md) for details. +* Scheduling passes for ARMv8 (aarch64) and RISC-V. * Some general-purpose optimization phases (e.g. profiling). * see [`PROFILING.md`](PROFILING.md) for details on the profiling system @@ -28,13 +29,24 @@ The people responsible for this version are * Sylvain Boulmé (Grenoble-INP, Verimag) * David Monniaux (CNRS, Verimag) * Cyril Six (Kalray) +* Léo Gourdin (UGA, Verimag) + +with contributions of: + +* Justus Fasse (M2R UGA, now at KU Leuven). +* Pierre Goutagny and Nicolas Nardino (L3 ENS-Lyon). ## Papers, docs, etc on this CompCert version * [a 5-minutes video](http://www-verimag.imag.fr/~boulme/videos/poster-oopsla20.mp4) by C. Six, presenting the postpass scheduling and the KVX backend (also on [YouTube if you need subtitles](https://www.youtube.com/watch?v=RAzMDS9OVSw)). +* [the documentation of the KVX backend Coq sources](https://certicompil.gricad-pages.univ-grenoble-alpes.fr/compcert-kvx). * [Certified and Efficient Instruction Scheduling](https://hal.archives-ouvertes.fr/hal-02185883), an OOPSLA'20 paper, by Six, Boulmé and Monniaux. -* [the documentation of the KVX backend Coq sources](https://certicompil.gricad-pages.univ-grenoble-alpes.fr/compcert-kvx) +* [Formally Verified Superblock Scheduling](https://hal.archives-ouvertes.fr/hal-03200774), a CPP'22 paper, by Six, Gourdin, Boulmé, Monniaux, Fasse and Nardino. +* [Optimized and formally-verified compilation for a VLIW processor](https://hal.archives-ouvertes.fr/tel-03326923), Phd Thesis of Cyril Six in 2021. +* [Formally Verified Defensive Programming (efficient Coq-verified computations from untrusted ML oracles) -- Chapters 1 to 3](https://hal.archives-ouvertes.fr/tel-03356701), Habilitation Thesis of Sylvain Boulmé in 2021. +* [Code Transformations to Increase Prepass Scheduling Opportunities in CompCert](https://www-verimag.imag.fr/~boulme/CPP_2022/FASSE-Justus-MSc-Thesis_2021.pdf), MSc Thesis of Justus Fasse in 2021. +* [Register-Pressure-Aware Prepass-Scheduling for CompCert](https://www-verimag.imag.fr/~boulme/CPP_2022/NARDINO-Nicolas-BSc-Thesis_2021.pdf), BSc Thesis of Nicolas Nardino in 2021. ## License CompCert is not free software. This non-commercial release can only -- cgit