Extension paramétrée de compilateur certifié pour la programmation parallèle. (Parameterised extension of certified compiler for parallel programming). - Sylvain Dailler (2015)

Lightweight Interactive Proving inside an Automatic Program Verifier. - Sylvain Dailler; Claude Marché; Yannick Moy (F-IDE@FLoC, 2018)

Instrumenting a weakest precondition calculus for counterexample generation. - Sylvain Dailler; David Hauzar; Claude Marché; Yannick Moy (J. Log. Algebraic Methods Program., 2018)