News

Matthias Függer et al: new article in JACM

How fast can you converge towards a consensus value?

In their recent work, Matthias Fuegger (LMF), Thomas Nowak (LISN), and Manfred Schwarz (TU Wien) study this question in distributed systems where nodes start from an initial value and seek to converge towards a common consensus value. The paper shows that deceptively simple algorithms are optimal and provides tight lower bounds.

Out now in JACM: 1145/3485242

Journées du GT Verif

ENS Paris-Saclay

Les Journées du GT Vérification du GDR IM ont lieu les 17, 18 et 19 novembre 2021 au Laboratoire Méthodes Formelles, ENS Paris-Saclay, à Gif-sur-Yvette.

Elles visent à rassembler la communauté française en vérification formelle, et en particulier les chercheurs juniors, doctorants et post-doctorants, avec pour objectif de favoriser les collaborations et l'ouverture sur des thématiques liées à la vérification. Elles ont pour ambition de couvrir tous les domaines de la vérification formelle.

Pour en savoir plus

PhD Defense: Mathilde Boltenhagen

Process Instance Clustering based on Conformance Checking Artefacts
by Mathilde Boltenhagen
Thursday 21 October 2021 at 10h15
Room 2Z81 ENS Paris-Saclay as well as online

Zoom link: us/j/95623460694
Passcode: FhrK69

Mathilde Boltenhagen

Abstract: As event data becomes an ubiquitous source of information, data science techniques represent an unprecedented opportunity to analyze and react to the processes that generate this data. Process Mining is an emerging field that bridges the gap between traditional data analysis techniques, like Data Mining, and Business Process Management. Read more...

PhD Defense: Anirban Majumdar

Verification and Synthesis of Parameterized Concurrent Systems
by Anirban Majumdar
Thursday 30 September 2021 at 14h00
Room 1Z68 ENS Paris-Saclay as well as online

Zoom link: us/j/99606315744
Meeting ID: 996 0631 5744
Passcode: anirb1

Anirban Majumdar

Abstract: This thesis is at the crossroad of verification and synthesis of parameterized concurrent systems. The parameterized model checking problem asks whether a system satisfies a given specification independently of the number of its components, whereas synthesis requires an algorithmic design of protocols for its components so that the specification is satisfied.Read more...

Caroline Fontaine dans Les décodeuses du numérique

La bande dessinée Les décodeuses du numérique vient de sortir. Conçu par l'INS2I du CNRS, l'ouvrage présente 12 portraits de chercheuses, enseignantes-chercheuses et ingénieures dans les sciences du numérique, illustrés par Léa Castor. Parmi les protagonistes rencontrez, dans le rôle d'agent spécial de la cybersécurité, notre collègue Caroline Fontaine.

La BD est disponible en ligne https://ins2i.cnrs.fr/fr/les-decodeuses-du-numerique.

Caroline Fontaine Takes the Lead of the CNRS Research Network on Computer Security

Caroline Fontaine at the CNRS-INS2I booth at FIC 2021

Caroline Fontaine has been appointed director of the CNRS Research Network on Computer Security GdR Securité Informatique in Summer 2021. The network federates the French research groups working on cryptography, formal methods for security, privacy, security of hardware, software, data and networks.

The photo shows Caroline at the International Cybersecurity Forum (FIC) on 7 - 9 September in Lille, where she presented the actions of the Network.

Best-Paper Award at FMICS 2021

Cláudio Belo Lourenço and Claude Marché from the Toccata team at LMF with co-authors from Mitsubishi Electric received the Best-Paper Award at FMICS 2021, the 26th International Conference on Formal Methods for Industrial Critical Systems. Read more...

Best-Paper Award at ICTAC 2021

Diaz, Dowek - ICTAC 2021 Best Paper Award

Gilles Dowek and Alejandro Díaz-Caro (Universidad de Buenos Aires and Universidad Nacional de Quilmes, Argentina) received the Best-Paper Award at ICTAC 2021, the 18th International Colloquium on Theoretical Aspects of Computing for their paper A New Connective in Natural Deduction, and Its Application to Quantum Computing.

PhD Defense: Yacine El Haddad

Integrating Automated Theorem Provers in Proof Assistants
by Mohamed Yacine El Haddad
Thursday 9 September 2021 at 14h00
online (link to be announced)

Abstract: Lambdapi is a proof assistant that allows users to construct a proof of a given theorem in a universal language based on the lambda-pi-calculus. The goal of this thesis is to add more automation to Lambdapi to save more time and effort for the users.Read more...

PhD defense : Jury Kolčák

Unfoldings and Abstract Interpretation for Parametric Biological Regulatory Networks
by Juraj Kolčák
Tuesday 06 July 2021 at 09h00, online

Jury:

  • Gilles Bernot (reviewer) – Université Nice Sophia Antipolis, Polytech Nice Sophia
  • Paolo Zuliani (reviewer) – Newcastle University
  • Pascale Le Gall – Centrale Supélec
  • Barbara König – Universität Duisburg-Essen
  • Heike Siebert – Freie Universität Berlin
  • Stefan Haar (PhD Supervisor) – Université Paris-Saclay