CompCert is a C compiler with a machine-checked mathematical proof of soundness. The Kalray K1c is a very large instruction word (VLIW) in-order core. We extend CompCert for the K1c core. For this, we need some optimizations such as instruction scheduling.
KALRAY-CompCert
We extend the CompCert certified compiler with a backend for the K1C core and various optimizations to reach high performance (instruction scheduling...).
Browsing
News
- Conferences
- Feb. 24, 2020 Workshop CAPITAL
- May 11-15, 2020 AlgoTel et CoRes 2020
- June 22-26, 2020 MOVEP 2020
- Seminars
- 16 December 2019 Lélio Brun: Verified compilation of the lustre modular reset
- 19 December 2019 Yannick Zakowski: From representing recursive and impure programs in coq to a modular formal semantics (...)
- 19 December 2019 Hang Yu: Towards an efficient parallel parametric linear programming solver (Phd)
- 6 February 2020 Jules Chouquet: Lower bounds for probabilistic k-set agreement through combinatorial (...)
Seminars
New publications
- Recent Publications
- Victor Magron, Alexandre Rocca, Thao Dang: Certified Roundoff Error Bounds using Bernstein Expansions and Sparse Krivine-Stengle Representations
- Stéphane Devismes, Anissa Lamani, Franck Petit, Sébastien Tixeuil: Optimal torus exploration by oblivious robots
- Moustapha Lo: Implementing a Real-time Avionic application on a Many-core Processor
- Karine Altisen, Pierre Corbineau, Stéphane Devismes: Squeezing Streams and Composition of Self-Stabilizing Algorithms
- Quentin Bramas, Stéphane Devismes, Pascal Lafourcade: Brief Announcement: Infinite Grid Exploration by Disoriented Robots
- Xiaojie Guo, Maxime Lesourd, Mengqi Liu, Lionel Rieg, Zhong Shao: Integrating Formal Schedulability Analysis into a Verified OS Kernel
