Lionel Blatter

About me

Since September 2022, I am a post-doctoral researcher at the Max Planck Institute for Security and Privacy, Bochum, Germany, in the group Foundation of Security and Privacy lead by Gilles Barthe.

Between January 2020 and July 2022, I was a post-doctoral researcher at Karlsruhe Institute of Technology (KIT), Karlsruhe, Germany, in the Application-oriented Formal Verification group lead by Prof. Dr. Bernard Beckert.

Between September 2018 and September 2019, I was ATER at Université Paris-Sud, Orsay.

Between Octobre 2015 and August 2018, I was a Phd student at University Paris Saclay France, under the supervision of Pascale Le Gall, Nikolai Kosmatov and Virgile Prevosto, at CEA-List Nano-INNOV and Centralesupelec in the MISC team. My PhD was about relational properties for specification and verification of C programs in Frama-C.

My research interests include formal methods, programming languages, safety and security of software and hardware.

Publications

• submitted 2025 The Jasmin Compiler Preserves Cryptographic Security.
  Santiago Arranz-Olmos, Gilles Barthe, Lionel Blatter, Benjamin Grégoire, Vincent Laporte, Paolo Torrini.
  [pdf]
• submitted 2025 (Dis)Proving Spectre Security with Speculation-Passing Style.
  Santiago Arranz-Olmos, Gilles Barthe, Lionel Blatter, Xingyu Xie, Zhiyuan Zhang.
  [pdf]
• submitted 2025 Decompiling for Constant-Time Analysis.
  Santiago Arranz-Olmos, Gilles Barthe, Lionel Blatter, Youcef Bouzid, Sören van der Wall, Zhiyuan Zhang.
  [pdf]
• CCS 2025 Jazzline: Composable CryptoLine functional correctness proofs for Jasmin programs.
  José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Lionel Blatter, Gustavo Delerue, João Diogo Duarte, Benjamin Gregoire, Tiago Oliveira, Miguel Quaresma, Pierre-Yves Strub, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang. (Distinguished Paper Award).
  [doi]
• POPL 2025 Preservation of Speculative Constant-Time by Compilation.
  Santiago Arranz Olmos, Gilles Barthe, Lionel Blatter, Benjamin Grégoire, Vincent Laporte.
  [doi] [pdf]
• ISoLA 2022 An Efficient VCGen-Based Modular Verification of Relational Properties.
  Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall, Virgile Prevosto.
  [doi] [pdf]
• IFM 2022 Certified Verification of Relational Properties.
  Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall, Virgile Prevosto.
  [doi] [pdf]
• TACAS 2022 Inferring Interval-Valued Floating-Point Preconditions.
  Jonas Krämer, Lionel Blatter, Eva Darulova, Mattias Ulbrich.
  [doi]
• PhD thesis 2019 Relational properties for specification and verification of C programs in Frama-C.
  Lionel Blatter
  [pdf]
• TAP 2018 Static and Dynamic Verification of Relational Properties on Self-composed C Code.
  Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall, Virgile Prevosto.
  [doi] [pdf]
• TACAS 2017 RPP: Automatic Proof of Relational Properties by Self-composition.
  Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall, Virgile Prevosto.
  [doi] [pdf]

Talk

• AFADL 2018 RPP : Preuve automatique de propriétés relationnelles par Self-Composition
  Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall, Virgile Prevosto.
  [pdf]

Books

• (WIP) Total Correctness.
  Lionel Blatter.
  Chapter in Volume 2: Programming Languages Foundations, of Software Foundation.
  [link]
• Specification and Verification of High-Level Properties.
  Lionel Blatter, Nikolai Kosmatov, Virgile Prevosto, Virgile Robles.
  Chapter in Guide to Software Verification with Frama-C. 2024
  [doi]

Research

Postdoc at Max Planck Institute

My research at the Max Planck Institute for Security and Privacy and Formosa Crypto can be resumed by the following items:

• (Speculative) Constant Time: Constant Time (CT) and Speculative Constant Time (SCT) are information flow policy that ensures that programs are protected against timing side-channel attacks (SCT consider Spectre attacks which exploide speculation of hardware). My research focused on the following points:
  • Proving compiler preservation of SCT (pdf).
  • Proving SCT using programme transformation (pdf).
  • Decompiling for CT analysis (pdf).
• Jasmin and Easycrypt: Jasmin is a certified compiler for writing high-assurance and high-speed cryptography code, and EasyCrypt is a proof assistant for Computer-Aided Cryptographic Proofs. My research focused primarily on the following points:
  • The Jazzline tooling for composable functional correctness proofs for Jasmin programs. The work combines the Jasmin compiler with Easycrypt and Cryptoline (pdf). This work inspired me to extend the nsatz tactic in Rocq, resulting in the ensatz tactic.
  • Formalizing cryptographic security with interaction trees and proving compiler preservation with relational hoare logic (pdf).
  • Currently, I'm working on the generation and verification of annotations for safty verification in Jasmin.
• Recently, I started to work on the Rocq library xhl, which includes the mecanization of different (probabilistic) (relational) hoare logics, and associate soundness and completness proofs.

Keywords: certified compilation, semantics of probabilistic programs, relational hoare logic, none-interference (constante time and speculative constante time), cryptography.

Postdoc at Karlsruhe Institute of Technology

My research at the Application-oriented Formal Verification group can be resumed by the following items:

• Formal verification of scientific software: Usually scientific software is written in low-level languages like C, uses message passing libraries for parallelisation, and relies on floating-point arithmetic for real abstraction. This implies that scientific software is susceptible to programming errors, and interesting for formal methods. My research focused on the following two points:

  • The developed of a tool called MPI-V, which combines multi-party session types and verification conditions generation for verifying the absence of deadlocks, session fidelity and functional correctness of distributed C programs (using MPI) for any number of participant.

  • An automatic synthesis of preconditions for floating-point functions. The generated preconditions guarantee that user-provided accuracy requirements are satisfied, i.e. avoiding unreliable numerical computations due to aggregated roundoff errors caused by floating-point arithmetic [3].

• Soundness proof of relational verification using verification condition generation: A formalization and soundness proofs, in the Coq proof assistant, of relational verification using verification condition generation and relational function contracts, for programs with recursive function calls and pointers [1], [2].

• Tain analysis for sh scripts: The developpement of a tool for taint analysis of shell scripts. The tool checks for information leakage using a user-specified definition of leakage.

Keywords: deductive verification, distributed programs, multi-party session types, relational hoare logic, floating point computations, taint analysis.

Phd thesis

During my PhD I worked on the formal verification of relational properties. My research focused on the support of relational properties in the Frama-C platform i.e. in the context of the C language and the specification language ACSL. The work can be summarised by the following points:

• Extention for the ACSL specification language to support relational properties.
• Design of relational contract based verification approaches, that can be integrated into standard contract based verification of programs.
• Implementation of the two previous points into a Frama-C plugin called RPP [4], [5].

Teaching

• 2025 Lecture on Total Correctness, Ruhr University Bochum, Germany. link.
• 2018-2019 Introduction to Logic, University Paris-Sud, Orsay, France.
• 2018-2019 Security of information and communication systems, University Paris-Sud, Orsay, France
• 2018-2019 Introduction to object programming, University Paris-Sud, Orsay, France.
• 2018-2019 Introduction to imperative programming, University Paris-Sud, Orsay, France.
• 2018-2019 Advanced imperative programming, University Paris-Sud, Orsay, France.
• 2018-2019 Introduction to functional programming, University Paris-Sud, Orsay, France.
• 2018-2019 Introduction to computer graphics, University Paris-Sud, Orsay, France.
• 2016-2018 Lecture on Constraint programming in Prolog, ISTY (Univ. Versailles-SQY), Vélizy, France (git).
• 2016-2017 Deductive verification with Frama-C, ENSIIE in Evry, France.
• 2016-2017 Introduction to object programming, UPEC in Créteil, France.

Supervision

• 2025 Co-supervised the internship of Prema Narayan Ochoa, on automatic generation of certified annotations for the Jasmin compiler.
• 2025 Co-supervised the internship of Jieyu Zheng, on adding support for AVX512 instruction to the Jasmin compiler.
• 2024 Co-supervised the internship of Parmida Javadian, on automatic generation of selective Speculative Load Hardening protections for the Jasmin compiler.
• 2021-2022 Supervised the Bachelor-Thesis of Maximilian von Gaisberg. "Formal Verificationn of Sorting Algorithms with Frama-C".
• 2021 Supervised the research internship of Tobias Hombücher "Verification of distributed system with Frama-C/MPIV".
• 2020-2021 Co-supervised the Master-Thesis of Jonas Krämer. "Inferring Interval-Valued Floating-Point Preconditions".

Contact