News & Events

The 6th edition of the Workshop on Automata, Concurrency, and Timed Systems will take place from 30 May to 2 June 2023 at ENS Paris-Saclay.

The workshop series emerged from a long-standing Indo-French cooperation in the areas of ACTS: Automata and Logic, Concurrency Theory, and Timed Systems.

As a special event, this year's programme features a session in honour of Paul Gastin on the occasion of his retirement.

For information on the programme and registration, visit the workshop page.

Oct 12 14:00 ₂₀₂₃

Read more...

Jul 4 14:00 ₂₀₂₃

Résumé : La présente thèse se situe à l'intersection des méthodes formelles et des bases de données, et s'intéresse à la formalisation de la provenance des données à l'aide de l'assistant de preuve Coq. L'étude de la provenance des données, qui permet de retracer leur origine et leur historique, est essentielle pour assurer la qualité des données, éviter les interprétations erronées et favoriser la transparence dans le traitement des données. Read more...

Les journées du LMF 2023 vont avoir lieu les 12 – 13 juin 2023 au Étiolles Country Club.

How to get there

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

• Monday, meeting 9h20 at the Digiteo parking (rue Raimond Castaing), departure 9h30; a second stop at Le Guichet RER station
• Tuesday, departure at 16h45 from Étiolles Country Club towards Le Guichet RER station, 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, Monday 12 June

10h30 – 11h00 Arrival, welcome coffee

11h00 – 12h30 Tutorial (salle Varangues)

• Stéphane Demri: Introduction to Temporal Logics with Concrete Domains

12h30 – 14h00 Lunch

14h00 – 15h30 Science Talks (salle Varangues)

• Me & my project: Gustave Cortal, Marc Renard, Nicolas Heurtel, Rishikesh Vaishnav
• Lina Ye: Analyzing Robustness of Angluin's L* Algorithm in Presence of Noise (30 minutes)
• Guillaume Scerri: tba (30 minutes)

15h30 – 16h00 Coffee break

16h00 – 18h00

• Team building (murder party)

18h00 – 20h00

• Get your room key

20h00 Dinner

Day 2, Tuesday 13 June

8h00 – 8h45

• Breakfast
• Give your room key back

9h00 – 10h30 Tutorial (salle Varangues)

• Jean Goubault-Larrecq: A journey through the semantics of higher-order probabilistic languages,domain theory, and topology

10h30 – 11h00 Coffee break

11h00 – 12h30 Discussion / ateliers (salle Varangues)

• Retour sur l'atelier psychodynamique du travail -- Thomas Chatain (30 minutes)
• Régulation des émotions par leur compréhension -- Alain Finkel (45 minutes)
• Développement durable -- Thomas Chatain (15 minutes)

12h30 – 14h00 Lunch

14h00 – 16h00 Science talks (salle Varangues)

• Me & my project: Quentin Petitjean, Benoit Ballenghien, Paul Geneau de Lamarliere, Kinnari Dave
• Thomas Nowak: Topological Simplicial Complexes for Task Solvability in Distributed Systems (30 minutes)
• Thibaut Balabonski : Normalization by need: a case study in reasoning on binders (30 minutes)
• Esteban Castro Ruiz: A perspective on quantum causal structures (30 minutes)

16h00 – 16h30 Coffee break, departure

Congratulations to Jacques-Henri Jourdan and his co-authors who will receive the 2023 Alonzo Church Award for their outstanding contributions to Logic and computation with the design and implementation of Iris, a higher-order concurrent separation logic framework. The Award will be presented at the 50th EATCS International Colloquium on Automata, Languages and Programming, ICALP 2023, in July.

Iris has been widely used in academia, and also in industry, e.g., by engineers at Meta to verify the core components of an interprocess communication system for a new operating system.

Read more...

Dr. Achim Brucker is a full Professor in Computer Science (Chair of Cybersecurity) at the University of Exeter, UK and a leading expert in secure software engineering, cyber security, and formal methods. He is the head of the Cybersecurity Group at Exeter and leads the Software Assurance & Security Research Team. From December 2015 to May 2019, he was a Senior Lecturer and Consultant at the Computer Science Department of The University of Sheffield, UK.

Achim will visit the LMF in the period from the 8th of May to the 8th of June. Besides his collaborations in the field of Ontology-based Modelling and Formal Software Engineering, three major presentations are planned:

• a keynote seminar on Computer Security on 16 May;
• a talk on Neural Network Verification in the GT Formal AI;
• a workshop on theoretical and practical Computer Security to the end of his visit, addressing PhD students and postdocs.

Jean-​Christophe Filliâtre and Andrei Paskevich have been awarded the prize for the Best Contributed Problem at this year's VerifyThis Competition held as a satelite event of ETAPS 2023.

VerifyThis is a series of program verification competitions, which takes place annually since 2011. The competition offers a number of challenges presented in natural language and pseudocode. Participants have to formalise the requirements, implement a solution, and formally verify the implementation for adherence to the specification.

Apr 26 16:00 ₂₀₂₃

Abstract: We study two-player zero-sum turn-based games on graphs, a framework of choice in theoretical computer science. Such games model the possibly infinite interaction between a computer system (often called reactive) and its environment. Read more...

Gilles Dowek vient d'être nommé au Conseil supérieur des programmes.

Lire l'article

Mar 16 :00 ₂₀₂₃

Larencontre annuelle du groupe de travail MTV2 Méthodes de Test pour la Vérification et la Validation sera organisée au LMF par Burkhart Wolff, Frédéric Voisin et Fatiha Zaidi le 16 mars 2023,

Read more...

Jan 13 15:00 ₂₀₂₃

Abstract: The advent of quantum computers capable of solving problems that are intractable on classical computers has motivated the development of new programming languages and tools for quantum computing. However, the current state of the art in quantum programming is still in its infancy.

In this thesis, we present a series of novel approaches to different aspects of the quantum compilation process based on the ZX calculus. Read more...

Dec 14 14:00 ₂₀₂₂

Abstract: Multicore OCaml extends OCaml with support for shared-memory concurrency. It is equipped with a weak memory model, for which an operational semantics has been published. This begs the question: what reasoning rules can one rely upon while writing or verifying Multicore OCaml code?

To answer it, we instantiate Iris, a modern descendant of Concurrent Separation Logic, for Multicore OCaml. This yields a low-level program logic whose reasoning rules expose the details of the memory model. On top of it, we build a higher-level logic, Cosmo, which trades off some expressive power in return for a simple set of reasoning rules that allow accessing non-atomic locations in a data-race-free manner, exploiting the sequentially-consistent behavior of atomic locations, and exploiting the release/acquire behavior of atomic locations. Cosmo allows both low-level reasoning, where the details of the Multicore OCaml memory model are apparent, and high-level reasoning, which is independent of this memory model.

Read more...