Dr. Lionel Blatter

Wissenschaftlicher Mitarbeiter

Raum 227, Gebäude 50.34
Tel.: +49 721 608-43856
Fax: +49 721 608-44021
lionel blatterXwx3∂kit edu
KIT / Institut für Theoretische Informatik

Am Fasanengarten 5
Gebäude 50.34
76131 Karlsruhe
Deutschland


Tools and Formal Proofs

  • Frama-C-MPI-V - Session Types based Verification of distributed C programs.
  • Frama-C-RPP - Modular Relational Verification of C programs.
  • Relational-Spec - Coq formalization of Relational Properties Verification.

Publications

2022
Titel Autor(en) Quelle
Certified Verification of Relational PropertiesLionel Blatter, Nikolai Kosmatov, Virgile Prevosto und Pascale Le Gall17th International Conference on integrated Formal Methods (iFM 2022)
Inferring Interval-Valued Floating-Point PreconditionsJonas Krämer, Lionel Blatter, Eva Darulova und Mattias Ulbrich28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2022), held as part of ETAPS 2022: European Joint Conferences on Theory and Practice of Software, Teil I
2019
Titel Autor(en) Quelle
Relational properties for specification and verification of C programs in Frama-CLionel BlatterUniversité Paris-Saclay (September 2019)
2018
Titel Autor(en) Quelle
Static and Dynamic Verification of Relational Properties on Self-composed C CodeLionel Blatter, Nikolai Kosmatov, Pascale Le Gall, Virgile Prevosto und Guillaume Petiot12th International Conference on Tests and Proofs (TAP 2018) held as part of STAF 2018: Software Technologies - Applications and Foundations
Self-composition to Prove Relational Properties in Annotated C ProgramLionel Blatter, Nikolai Kosmatov, Pascale Le Gall und Virgile PrevostoCoRR abs/1801.06876
2017
Titel Autor(en) Quelle
RPP: Automatic Proof of Relational Properties by Self-compositionLionel Blatter, Nikolai Kosmatov, Pascale Le Gall und Virgile Prevosto23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2017) held as part of ETAPS 2017: European Joint Conferences on Theory and Practice of Software, Teil I
2016
Titel Autor(en) Quelle
Deductive Verification with Relational PropertiesLionel Blatter, Nikolai Kosmatov, Pascale Le Gall und Virgile PrevostoCoRR abs/1606.00678