News & Events
Gilles Dowek lauréat du Grand prix Inria - Académie des sciences 2023
Le Grand prix 2023 Inria-Académie des sciences a été décerné à Gilles Dowek.
Parallèlement à ses travaux scientifiques et techniques, Gilles Dowek a contribué à la construction d'une philosophie naissante de l'informatique, qui se construit dans un dialogue entre philosophes et scientifiques. Il s'est, en particulier, intéressé à la place du calcul en mathématiques, à la différence entre les langues et les langages et aux rapports entre la thèse de Church-Turing et celle de Galilée.— Citation du prix
Le Prix Inria – Académie des sciences récompense depuis 2013 une ou un scientifique ayant contribué de manière exceptionnelle au champ des sciences informatiques et mathématiques.
PhD Defence: Georges Aazan
Stability of constrained switched systems driven by ω-regular languages
by Georges Aazan
Friday 27 October 2023 at 2pm
ENS Paris-Saclay, Room 1Z14 and Zoom
Abstract. Switched systems are dynamical systems with several operating modes, each mode being described by a differential (continuous time) or difference (discrete time) equation. Read more...
Soutenance de thèse : Clément Pascutto
Runtime Verification of OCaml Programs
Mercredi 18 octobre 2023 14h
Université Paris-Saclay, bâtiment 660, salle 40 (amphi)
Formal verification methods, in particular when it comes to deductive verification, bring strong guarantees about the correctness of software systems. However, they require a high degree of expertise and tremendous development time. Read more...
PhD Defence: Benjamin Bordais
Concurrent two-player antagonistic games on graphs
by Benjamin Bordais
Thursday 12 October 2023 at 2PM
ENS Paris-Saclay, room 1Z56
Abstract. We study two-player antagonistic games on graphs. In such a setting, two players, Player A and Player B, start at a given state of a graph and then concurrently interact to choose a probability distribution over successor states. This process is then repeated indefinitely, thus creating an infinite sequence of states: the outcome of game. That outcome is mapped by a payoff function to a value between 0 and 1 that Player A wants to maximize, while Player B wants to minimize it.
Soutenance de thèse : Aliaume Lopez
First Order Preservation Theorems in Finite Model Theory : Locality, Topology, and Limit Constructions
par Aliaume Lopez
Mardi 12 septembre 2023 à 14h
Université Paris-Cité, Bâtiment Olympe de Gouges, salle 127
Soutenance de thèse : Rébecca Zucchini
Bibliothèque certifiée en Coq pour la provenance des données
par Rébecca Zucchini
Mardi 4 juillet 2023 à 14h
ENS Paris-Saclay, salle 1Z14
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...
Alonzo Church Award 2023 for Jacques-Henri Jourdan
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.
Invited Visit of Achim Brucker
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 win VerifyThis Competition
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.