Lionel Blatter

15 papers A* 1B 1Journal 9Unranked 4
YearRankTypeTitle / Venue / Authors
2025 J jnl
(Dis)Proving Spectre Security with Speculation-Passing Style.
CoRR
Santiago Arranz-Olmos, Gilles Barthe, Lionel Blatter, Xingyu Xie, Zhiyuan Zhang
2025 A* conf
Jazzline: Composable CryptoLine Functional Correctness Proofs for Jasmin Programs.
CCS
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Lionel Blatter, Gustavo Xavier Delerue Marinho Alves, João Diogo Duarte, Benjamin Grégoire, Tiago Oliveira, Miguel Quaresma, Pierre-Yves Strub, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang
2025 J jnl
Preservation of Speculative Constant-Time by Compilation.
Proc. ACM Program. Lang.
Santiago Arranz-Olmos, Gilles Barthe, Lionel Blatter, Benjamin Grégoire, Vincent Laporte
2025 J jnl
The Jasmin Compiler Preserves Cryptographic Security.
CoRR
Santiago Arranz-Olmos, Gilles Barthe, Lionel Blatter, Benjamin Grégoire, Vincent Laporte, Paolo Torrini
2025 J jnl
Transparent Decompilation for Timing Side-Channel Analyses.
CoRR
Santiago Arranz-Olmos, Gilles Barthe, Lionel Blatter, Sören van der Wall, Zhiyuan Zhang
2024 J jnl
An Efficient VCGen-based Modular Verification of Relational Properties.
CoRR
Lionel Blatter, Nikolai Kosmatov, Virgile Prevosto, Pascale Le Gall
2024 J jnl
Preservation of Speculative Constant-time by Compilation.
IACR Cryptol. ePrint Arch.
Santiago Arranz-Olmos, Gilles Barthe, Lionel Blatter, Benjamin Grégoire, Vincent Laporte
2022 — conf
An Efficient VCGen-Based Modular Verification of Relational Properties.
ISoLA (1)
Lionel Blatter, Nikolai Kosmatov, Virgile Prevosto, Pascale Le Gall
2022 B conf
Certified Verification of Relational Properties.
IFM
Lionel Blatter, Nikolai Kosmatov, Virgile Prevosto, Pascale Le Gall
2022 J jnl
Certified Verification of Relational Properties.
CoRR
Lionel Blatter, Nikolai Kosmatov, Virgile Prevosto, Pascale Le Gall
2022 — conf
Inferring Interval-Valued Floating-Point Preconditions.
TACAS (1)
Jonas Krämer, Lionel Blatter, Eva Darulova, Mattias Ulbrich
2018 J jnl
Self-composition to Prove Relational Properties in Annotated C Program.
CoRR
Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall, Virgile Prevosto
2018 — conf
Static and Dynamic Verification of Relational Properties on Self-composed C Code.
TAP@STAF
Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall, Virgile Prevosto, Guillaume Petiot
2017 — conf
RPP: Automatic Proof of Relational Properties by Self-composition.
TACAS (1)
Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall, Virgile Prevosto
2016 J jnl
Deductive Verification with Relational Properties.
CoRR
Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall, Virgile Prevosto