A noter que CompCert est utilisé comme base de nombreux autres projets de recherche/industriels, notamment le projet Verified Toolchain (qui fait parti du projet plus grand DeepSpec) qui vise à avoir la maîtrise complète de chaîne de compilation : http://vst.cs.princeton.edu/
DeepSpec vise à atteindre la même maîtrise, mais sur un écosystème entier : http://deepspec.org/
Ca passe par un noyau et un OS formellement vérifiés (CertikOS), et d'autres choses.
# Verified toolchain
Posté par Harvesterify . En réponse au journal Xavier Leroy est le lauréat 2016 du Prix Milner.. Évalué à 9.
A noter que CompCert est utilisé comme base de nombreux autres projets de recherche/industriels, notamment le projet Verified Toolchain (qui fait parti du projet plus grand DeepSpec) qui vise à avoir la maîtrise complète de chaîne de compilation : http://vst.cs.princeton.edu/
DeepSpec vise à atteindre la même maîtrise, mais sur un écosystème entier : http://deepspec.org/
Ca passe par un noyau et un OS formellement vérifiés (CertikOS), et d'autres choses.
Mes messages engagent qui je veux.