Publications

2023

• Jean-Christophe Léchenet, Nikolai Kosmatov, Pascale Le Gall.
  Efficient computation of arbitrary control dependencies.
  In Theoretical Computer Science.
  [doi] [pdf] [website] [code]
• Benjamin Grégoire, Jean-Christophe Léchenet, Enrico Tassi.
  Practical and Sound Equality Tests, Automatically: Deriving eqType Instances for Jasmin's Data Types with Coq-Elpi.
  In CPP 2023.
  [doi] [HAL] [pdf] [slides]

2020

• Jean-Christophe Léchenet, Sandrine Blazy, David Pichardie.
  A Fast Verified Liveness Analysis in SSA form.
  In IJCAR 2020.
  [doi] [pdf] [website] [slides]

2018

• Jean-Christophe Léchenet.
  Certified Algorithms for Program Slicing.
  PhD thesis, Université Paris-Saclay.
  [DART-Europe] [pdf] [slides]
• Jean-Christophe Léchenet, Nikolai Kosmatov, Pascale Le Gall.
  Cut branches before looking for bugs: certifiably sound verification on relaxed slices.
  In Formal Aspects of Computing.
  [doi] [pdf] [website]
• Jean-Christophe Léchenet, Nikolai Kosmatov, Pascale Le Gall.
  Fast Computation of Arbitrary Control Dependencies.
  In FASE 2018 (part of ETAPS 2018).
  [doi] [pdf] [website] [slides] [code]
• Jean-Christophe Léchenet, Nikolai Kosmatov, Pascale Le Gall.
  Why3 a dit : gardez le contrôle en toute situation.
  In JFLA 2018. (In French).
  [HAL] [pdf] [website] [slides]

2016

• Jean-Christophe Léchenet, Nikolai Kosmatov, Pascale Le Gall.
  Cut Branches Before Looking for Bugs: Sound Verification on Relaxed Slices.
  In FASE 2016 (part of ETAPS 2016).
  [doi] [pdf] [website] [slides]
• Jean-Christophe Léchenet, Nikolai Kosmatov, Pascale Le Gall.
  Coq a dit : fromage tranché ne peut cacher ses trous.
  In JFLA 2016. (In French).
  [HAL] [pdf] [website] [slides]