Deductive Verification with Relational Properties. - Lionel Blatter; Nikolai Kosmatov; Pascale Le Gall; Virgile Prevosto (CoRR, 2016)

RPP: Automatic Proof of Relational Properties by Self-composition. - Lionel Blatter; Nikolai Kosmatov; Pascale Le Gall; Virgile Prevosto (TACAS (1), 2017)

Static and Dynamic Verification of Relational Properties on Self-composed C Code. - Lionel Blatter; Nikolai Kosmatov; Pascale Le Gall; Virgile Prevosto; Guillaume Petiot (TAP@STAF, 2018)

Self-composition to Prove Relational Properties in Annotated C Program. - Lionel Blatter; Nikolai Kosmatov; Pascale Le Gall; Virgile Prevosto (CoRR, 2018)

Certified Verification of Relational Properties. - Lionel Blatter; Nikolai Kosmatov; Virgile Prevosto; Pascale Le Gall (IFM, 2022)

An Efficient VCGen-Based Modular Verification of Relational Properties. - Lionel Blatter; Nikolai Kosmatov; Virgile Prevosto; Pascale Le Gall (ISoLA (1), 2022)

Inferring Interval-Valued Floating-Point Preconditions. - Jonas Krämer; Lionel Blatter; Eva Darulova; Mattias Ulbrich (TACAS (1), 2022)

Preservation of Speculative Constant-Time by Compilation. - Santiago Arranz-Olmos; Gilles Barthe; Lionel Blatter; Benjamin Grégoire; Vincent Laporte (Proc. ACM Program. Lang., 2025)

Transparent Decompilation for Timing Side-Channel Analyses. - Santiago Arranz-Olmos; Gilles Barthe; Lionel Blatter; Sören van der Wall; Zhiyuan Zhang 005 (CoRR, 2025)