News & Events

Hubert Comon Retirement Workshop

Hubert Comon has just retired. A celebration workshop in his honour will take place at ENS Paris-Saclay in the "Grand Amphithéâtre" on June 16, 2022. The event is joint with the final meeting of the ANR TECAP project.

Hubert Comon

Read more...

Seminaire au vert, Étiolles, 9 – 10 juin 2022

Les journées du LMF 2022 vont avoir lieu les 9 – 10 juin 2022 au Étiolles Country Club.

How to get there

A bus leaving from Gif-sur-Yvette to Étiolles on Thursday morning, returning on Friday evening:

  • Thursday, meeting 9h30 at the Digiteo parking (rue Raimond Castaing), departure 9h45; no stop in Guichet this time !
  • Friday, departure at 16h30 from Étiolles Country Club towards Le Guichet RER, with terminus Digiteo parking.

If you arrange your own transport (car, bike, public transportation), please check the arrival instructions of our host.

For those arriving by RER, a shuttle service will be running from the RER D station Evry Val de Seine to Étiolles Country Club between 10h and 10h30.

Programme


Day 1, Thursday 9 June


10h30 – 11h00 Arrival, welcome coffee

11h00 – 12h30 Tutorial (salle Birdy)

  • Andrei Paskevich and Jean-Christophe Filliâtre: Why3

12h30 – 14h00 Lunch

14h00 – 15h30 Science Talks (salle Birdy)

  • Me & my project: Kostia Chardonnet, Agustin Borgna, Julien Simonnet (10 minutes each)
  • Stéphane Demri: Dynamic Axioms in Description Logics (30 minutes)
  • Jacques-Henri Jourdan: Verifying Rust programs using Creusot (30 minutes)

15h30 – 16h00 Coffee break

16h00 – 18h00 Discussion / ateliers (salle Birdy)

  • Présentation du projet d'échanges linguistiques (Fabricio Cravo Gomes)
  • Présentation du projet de posters (Mihaela Sighireanu)
  • Proposition d'atelier « design de t-shirts » (Amrita Suresh)
  • Possibly something else

18h00 – 20h00

  • Get your room key
  • Apéro italien (Milano Country Club)

20h00 – 22h00 Dinner

From 22h Soirée Casino Bling Bling (Club House)


Day 2, Friday 10 June


8h00 – 8h45

  • Breakfast
  • Give your room key back

9h00 – 10h30 Tutorial (salle Varangues)

  • Benedikt Bollig: Automata learning

10h30 – 11h00 Coffee break

11h00 – 12h30 Discussion + photos individuelles + photo de groupe (salle Varangues)

12h30 – 14h00 Lunch

14h00 – 16h00 Science talks (salle Varangues)

  • Me & my project: Fabricio Cravo Gomes, Luc Chabassier, Louise Dubois de Prisque (10 minutes each)
  • Armaël Guéneau: Separation Logic: beyond Functional Correctness (30 minutes)
  • Laurent Doyen: Stochastic Games with Synchronizing Objectives (30 minutes)
  • Vladimir Zamdzhiev: Quantum Expectation Transformers for Cost Analysis (30 minutes)

16h00 – 16h30 Coffee break, departure

Portraits de chercheurs : Stefan Haar

Stefan Haar

Repousser les limites des systèmes à événements discrets : un article sur notre collègue Stefan Haar vient de paraitre dans la rubrique Portraits de chercheurs des Actualités de l'Université Paris-Saclay.

Lire l'article

ACM Software System Award for Jacques-Henri Jourdan / CompCert

Association for Computing Machinery (ACM) logo

Jacques-Henri Jourdan receives the 2021 ACM Software System Award together with Xavier Leroy, Sandrine Blazy, Zaynah Dargaye, Michael Schmidt, Bernhard Schommer, and Jean-Baptiste Tristan for their work on the CompCert formally verified compiler.

Read more...

PhD Defence: Lulu He

Formal verification at design stage of diagnosis related properties for discrete event and real-time systems
by Lulu He
Wednesday 18 May 2022 at 10am
Room 435 (salle des thèses), building 650, 6 Rue Noetzlin, 91190 Gif-sur-Yvette.

Lulu He

Abstract: Fault diagnosis is a crucial and challenging task in the automatic control of complex systems, whose efficiency depends on a system property called diagnosability. Diagnosability describes the system property allowing one to determine at design stage whether a given fault occurring online will be identifiable with certainty based on the available observations, which is an alternative to testing that can only show the presence of failures without guaranteeing their absence. Read more...

New Project on Safety in Autonomous Cars

“How can we model autonomous cars in the most general way and establish the absence of catastrophic events? How to preserve such safety properties under extensions of the model?" This question marked the beginning of a fruitful partnership with SystemX on projects like SVR and now 3SA involving industrial partners such as transdev, Renault and PSA.

Read more...

Science ouverte : Prix pour Coq

L'assistant de preuves Coq est d'abord un langage informatique qui permet d'écrire des définitions et des énoncés mathématiques, de décrire des structures de données informatiques et des algorithmes. Il s’agit aussi d’un environnement pour développer des preuves de théorèmes complètement vérifiées par l'ordinateur, par exemple, la correction d'un algorithme. Read more...

Nouveau prix de thèse pour Charlie Jacomme

Charlie Jacomme, ancien doctorant du LSV, obtient un accessit du Prix de thèse Gilles Kahn de la Société Informatique de France (SIF) pour sa thèse Proofs of Security Protocols - Symbolic Methods and Powerful Attackers. Cette nouvelle récompense s'ajoute au Prix de thèse du GDR Sécurité attribué à Charlie en 2021.

PhD Defence: Igor Khmelnitsky

Verification of Infinite-State Systems and Machine Learning
by Igor Khmelnitsky
Thursday 27 January 2022 at 2pm
Room 1Z25, ENS Paris-Saclay and online

Igor Khmelnitsky

Abstract: This work consists of three parts. The first one is devoted to the verification of Petri nets, the second one to the verification of recursive Petri nets which extend Petri nets, and the final one aims at combining active learning and verification.Read more...

Soutenance de thèse : Quentin Garchery

Certification de la transformation de tâches de preuve
par Quentin Garchery
Mardi 25 janvier 2022 à 14h00
Salle 435 (salle des thèses), bâtiment 650 Ada Lovelace et en ligne

Quentin Garchery

Abstract: In various provers and deductive verification tools, logical transformations are used extensively in order to reduce a proof task into a number of simpler tasks. Logical transformations are often part of the trusted base of such tools. In this thesis, we develop a framework to improve confidence in their results. Read more...