LMF Offers/Opportunities

Postes Ouverts

Quatre postes d'EC au LMF en 2025

Quatre postes d'enseignant·e·s-chercheur·e·s avec affectation au LMF ouvrent en 2025 :

By patricia, on February 04, 2025, at 03:34 PM

Un poste d'enseignant·e-chercheur·e (professeur·e) à l'ENS Paris-Saclay

Un poste de professeur·e est ouvert dans le DER d'informatique de l'ENS Paris-Saclay, avec affectation au laboratoire LMF. Pour plus d'informations, veuillez s'il-vous-plaît vous référer au profil du poste.

By patricia, on January 31, 2025, at 09:31 AM

Un poste d'enseignant·e-chercheur·e (maître·sse de conférences) à Polytech, Université Paris-Saclay

Un poste de MCF est ouvert à Polytech, Université Paris-Saclay, avec affectation au laboratoire LMF. Pour plus d'informations, veuillez s'il-vous-plaît vous référer au profil du poste.

By patricia, on January 31, 2025, at 09:15 AM

Un poste d'enseignant·e-chercheur·e (professeur·e) à la Faculté des Sciences, Université Paris-Saclay

Un poste de professeur·e est ouvert dans le département d'informatique de la faculté des sciences, Université Paris-Saclay, avec affectation au laboratoire LMF. Pour plus d'informations, veuillez s'il-vous-plaît vous référer au profil du poste.

By patricia, on January 31, 2025, at 09:16 AM

Un poste d'enseignant·e-chercheur·e (maître·sse de conférences) à la Faculté des Sciences, Université Paris-Saclay

Un poste de MCF est ouvert dans le département d'informatique de la faculté des sciences, Université Paris-Saclay, avec affectation au laboratoire LMF. Pour plus d'informations, veuillez s'il-vous-plaît vous référer au profil du poste.

By patricia, on January 31, 2025, at 09:15 AM

Internship Offers

Signalling Strategies in Distributed Networks

Level: M1 – M2

Contact: Dietmar Berwanger (dwb@lmf.cnrs.fr) and Patricia Bouyer (bouyer@lmf.cnrs.fr)

Location: Laboratoire Méthodes Formelles, ENS Paris-Saclay

Keywords: Distributed synthesis, signalling, automata theory, imperfect information

Description

In distributed systems, control actions are often executed by a single component, but the information needed to make these decisions is dispersed across the system. This internship focuses on the synthesis of signalling strategies, where the objective is not to coordinate multiple control agents but to ensure that information is effectively transmitted within the system.

By dwb, on April 21, 2025, at 10:08 PM

Extending Isabelle/HOLBee with Support for Refinements

Level: L3 Info-Math, M1

Contact: Burkhart Wolff

Summary.HOL-Bee is a semantic Frontend for Abrial's Event-B Method in Isabelle/HOL. It permits to edit specifications in the Event-B language inside the eco-sytem of Isabelle (IDE, kernel, code-generator, proof-system, libraries) and to generate its semantic representation in form of state-relations.

In this internship, the objective is to extend this functionality by generating the proof-obligations and elementary proof-support. (Read the detailed internship proposal.).

By BurkhartWolff, on December 01, 2024, at 11:20 AM

Generating a User-Manual with and for Isabelle/DOF

Level: L3, M1

Contact: Burkhart Wolff<burkhart.wolff [at] universite-paris-saclay [dot] fr>, Idir Ait-Sadoune<idir.aitsadoune@centralesupelec.fr>

Location: Laboratoire Méthodes Formelles, Université Paris-Saclay

Keywords: Isabelle/HOL, Isabelle/DOF, Formal Document Generation

More Details: here

By BurkhartWolff, on March 09, 2024, at 11:41 AM

Extending Isabelle/HOLBee with Support for Refinements

Level: L3 Info-Math, M1

Contact: Burkhart Wolff

 In this internship, the objective is to extend this functionality by  generating the proof-obligations

and elementary proof-support. (Read the detailed internship proposal.).

By BurkhartWolff, on October 17, 2023, at 11:20 AM

Connecting Isabelle/C with Isabelle/Clean

Level: L3, M1, M2

Contact: Burkhart Wolff

Summary. Isabelle/C is a framework for C code in C11 syntax deeply integrated into the Isabelle/PIDE development environment. Our framework provides an abstract interface for verification back-ends to be plugged-in independently. The purpose of this stage is to develop a translation from C11-AST's generated in Isabelle/C to a semantic backend called Clean, a simple execution model for an imperative target language.

Read the detailed internship proposal.

By BurkhartWolff, on October 17, 2023, at 11:20 AM

Modeling Cyber-Physical Systems with HOL-CyberPhi

Modeling and analysis of cyber-physical systems is a challenge for formal methods and an active area of research. Initially developed for the analysis of the safety properties of autonomous vehicles (see [1]), the HOL-Cyberphy framework, based on the Isabelle/HOL proof assistant, has been generalized to model multi-agent cyber-physical systems. . The objective of this internship is to study this framework, notably based on the use of an Isabelle theory of Communicating Sequential Processes (see [2]), and to adapt it to the modeling of cyber-multi-agent systems. communicating physics, in order to analyze and prove their proper functioning properties. We can particularly draw inspiration from the work of André Platzer in this area (see [3]).

Missions:

Constitute a state of the art on the formal modeling of communicating cyber-physical multi-agent systems;
Take charge of the Isabelle HOL-CyberPhy framework, by creating some models of single and multi-agent cyber-physical systems;
Design a generic model of communicating cyber-physical multi-agent systems based on case studies to be identified, and propose an adaptation of the HOL-CyberPhy framework accordingly.

Bibliographic references on the subject:

[1] Paolo Crisafulli, Safouan Taha, Burkhart Wolff. Modeling and Proving Safety in Autonomous Cars Scenarios in HOL-CSP. Research Report 1, University Paris-Saclay; IRT SystemX, Palaiseau. 2021, pp.81. URL:
[2] Taha S., Ye L., Wolff B.: HOL-CSP Version 2.0. Archive of Formal Proofs (2019).
[3] Brieger, Marvin & Mitsch, Stefan & Platzer, André. (2023). Dynamic Logic of Communicating Hybrid Programs

The internship may lead to recruitment for a thesis, on the subject described here