Lionel Blatter

About me

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

Prior to my position a the Max Planck Institute, 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.

Before joining the Application-oriented Formal Verification group, I was a Phd student at University of Paris Saclay France, under the supervision of Pascale Le Gall, Nikolai Kosmatov and Virgile Prevosto.

Research

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

Postdoc at Max Planck Institute (September 2022-Januray 2023 and since november 2023)

I am currently working on the EasyCrypt tool for Computer-Aided Cryptographic Proofs and the Jasmin compiler. Both are part of the Formosa project.

Keywords: certified compiler, decompilation, semantics of probabilistic programs, iteraction trees, relational hoare logic, none-interference (constante time and speculative constante time).

Postdoc at Karlsruhe Institute of Technology (2020-July 2022)

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 correcness 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.

Phd thesis (2015-2020)

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].

Publications

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.
  In CCS 2025 (Distinguished Paper Award).
  
• Preservation of Speculative Constant-Time by Compilation.
  Santiago Arranz Olmos, Gilles Barthe, Lionel Blatter, Benjamin Grégoire, Vincent Laporte.
  In POPL 2025.
  [doi] [pdf]

2024

• Specification and Verification of High-Level Properties.
  Lionel Blatter, Nikolai Kosmatov, Virgile Prevosto, Virgile Robles.
  [doi]

2022

• An Efficient VCGen-Based Modular Verification of Relational Properties.
  Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall, Virgile Prevosto.
  In ISoLA 2022.
  [doi] [pdf]
• Certified Verification of Relational Properties.
  Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall, Virgile Prevosto.
  In IFM 2022.
  [doi] [pdf]
• Inferring Interval-Valued Floating-Point Preconditions.
  Jonas Krämer, Lionel Blatter, Eva Darulova, Mattias Ulbrich.
  In TACAS 2022.
  [doi]

2019

• Relational properties for specification and verification of C programs in Frama-C
  Lionel Blatter
  PhD thesis, Université Paris-Saclay.
  [pdf]

2018

• Static and Dynamic Verification of Relational Properties on Self-composed C Code.
  Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall, Virgile Prevosto.
  In TAP 2018.
  [doi] [pdf]

2017

• RPP: Automatic Proof of Relational Properties by Self-composition.
  Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall, Virgile Prevosto.
  In TACAS 2017.
  [doi] [pdf]

Talk

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

Teaching

• Small invited talk at Ruhr University Bochum on Total Correctness. The teaching material include a chapter based on Software fundation.

• "Assistant Temporaire à l'Ensegnement et la Recherche" (temporary teaching and research fellow) at Univ. Paris Sud, Orsay in Computer Science in 2019 (128 hours of lectures or 192 hours of "travaux dirigés" or 288 hours of "travaux pratiques" per year, or any equivalent combination).

  Teaching has been done in the following courses:

  • Introduction to Logic.
  • Security of information and communication systems.
  • Introduction to object programming.
  • Introduction to imperative programming.
  • Advanced imperative programming.
  • Introduction to functional programming.
  • Introduction to computer graphics.

• Lecture on Constraint programming in Prolog at ISTY (Univ. Versailles-SQY) in Vélizy (git).
• Various teaching activities in Computer Science at:
  • Karlsruhe Institute of Technology, Germany.
  • UPEC in Créteil, France.
  • ENSIIE in Evry, France.

Supervised Projects and Theses

• Bachelor-Thesis of Maximilian von Gaisberg. "Formal Verificationn of Sorting Algorithms with Frama-C." (git).
• Research internship of Tobias Hombücher "Verification of distributed system with Frama-C/MPIV".
• Master-Thesis of Jonas Krämer. "Inferring Interval-Valued Floating-Point Preconditions".

Contact