Seminar

Seminars related to Celtique’s research themes:

  • Celtique Seminar – internal only
  • 68NQRT – http://68nqrt.irisa.fr/
  • Sosysec – http://seminaire-dga.gforge.inria.fr/

Past sessions of the Épicure Seminar:

  • 2022/09/28 Thomas Genet, “Comprendre Ethereum/Solidity par la pratique”
  • 2022/09/21 Roméo La Spina (Inria Épicure), “Un analyseur flots de données pour le compilateur formellement vérifié CompCert” abstract
    Un compilateur vérifié est un compilateur accompagné d’une preuve qui montre que ce dernier n’introduit pas de bogue dans les programmes. Une référence du domaine est le compilateur CompCert du langage C, entièrement écrit et prouvé à l’aide de l’assistant de preuve Coq. CompCert est un compilateur non seulement vérifié, mais aussi optimisant ; ses performances en termes de temps d’exécution d’un programme compilé sont comparables à celles obtenues avec l’option `-O1` du compilateur de référence GCC (non vérifié).Plusieurs optimisations de CompCert utilisent une analyse flot de données, qui résout un ensemble d’équations grâce à un algorithme dû à Kildall. Cependant, selon la taille du treillis utilisé pour faire l’analyse, la convergence de l’algorithme peut nécessiter un temps extrêmement long. Un autre algorithme, développé par Bourdoncle, qui paramètre l’analyse par un ordre d’itération calculé au préalable, permet l’utilisation efficace d’opérateurs d’élargissement, solution classique pour pallier ce problème dans le domaine de l’interprétation abstraite. Nous avons donc choisi d’implémenter l’algorithme de Bourdoncle dans CompCert et de comparer ses performances à celles de l’algorithme de Kildall, à la fois en termes d’efficacité et en termes de précision de l’analyse.

Previously, at the Épicure seminar:

Comments are closed.