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 (Since september 2022)

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

Postdoc at Karlsruhe Institute of Technology (2020-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-2019)

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

2022

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

2019

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

2018

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

2017

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

Talk

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

Teaching

• "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