Internship Offers
Metabolic Pathway Analysis in the Presence of Biological Constraints
Level: M2
Contact: Philippe Dague (pdague@lmf.cnrs.fr)
Location: Laboratoire Méthodes Formelles, ENS Paris-Saclay
Keywords: Metabolic pathway analysis, models of cellular growth, thermodynamics, kinetics, regulation, convex polyhedral geometry, combinatorial optimization, ASP
Context
In the context of systems biology, the analysis of metabolic pathways is an essential step in studying the behavior of metabolic networks, which has important societal implications for human health (metabolic therapies) and biotechnology (designing cell factories to produce metabolites of interest to the agri-food industry, animal husbandry, energy production, and environmental protection).
Safety Analysis of Real-Time Discrete-Event and Hybrid Systems
Level: M2
Contact: Philippe Dague (pdague@lmf.cnrs.fr) and Lina Ye (lina.ye@centralesupelec.fr)
Location: Laboratoire Méthodes Formelles, ENS Paris-Saclay
Keywords: Safety analysis, diagnosability, timed automata, hybrid automata, abstraction, approximation
Context
More and more systems are safety-critical, e.g., medical devices, aircraft flight control, nuclear systems, and, more recently, cyber-physical systems. Verifying at the design stage safety properties is consequently crucial for their reliability. We are particularly interested in the diagnosability property [15], i.e., the ability to determine without ambiguity from the observations and within a given time delay that a given fault has occurred, i.e., to disambiguate faulty and normal trajectories from observations. Verifying diagnosability property boils down to proving the unsatisfiability of a logical formula [5, 14] expressing the existence of a so-called critical pair, i.e., a pair of faulty and normal trajectories, with enough long duration after the fault occurrence, sharing the same observations, which would violate diagnosability. For discrete-event systems, checking this formula can be done by using a Satisfiability (SAT) solver or a Satisfiability Modulo Theories [3] (SMT) solver (with Linear Real Arithmetic theory for dealing with time constraints) [8]. The major challenge for modeling and verifying these systems resides in their intrinsic complexity arising from the combination of a continuous part (analog physical processes) and a discrete part (digital computational processes), and the interaction between them. They can be modeled classically by hybrid automata [9], i.e., finite state machines with a finite set of continuous variables whose values are described by a set of ordinary differential equations, associated with the different states (or modes), the discrete transitions between states being in turn determined by the evolution of the continuous variables. Due to the continuous part, almost all problems, even the simplest, such as reachability, are undecidable for general hybrid automata. This shows that the use of approximations is necessary to check the safety properties of hybrid systems.
A New Semantics for Boolean Networks Based on Regulatory Threshold Constraints Consistency
Level: M2
Contact: Philippe Dague (pdague@lmf.cnrs.fr) and Thomas Chatain (chatain@lmf.cnrs.fr)
Location: Laboratoire Méthodes Formelles, ENS Paris-Saclay
Keywords: Boolean Networks, Constraint satisfiability
Context
Since their introduction in the late 1960s [9], logical models, such as Boolean Networks (BNs), have been widely adopted for reasoning about signaling and gene networks as they require few parameters and can easily integrate information from omics datasets and genetic screens. These models represent processes with a high degree of generalization and can offer coarse-grained but robust predictions, which makes them particularly suitable for large biological networks. BNs are formal discrete dynamical systems with notorious applications for modeling cellular differentiation and fate decision processes: the attractors capture the stable behaviors, and the trajectories capture the transient dynamics of the cell. To each BN is attached its interaction graph that references the positive and negative influences between components and hence is a compact and static abstraction of the BN dynamics [6]. Also, methods based on a generalization of the steady state notion, the so- called trap spaces, can be exploited to investigate attractor properties as well as for model reduction techniques [3].
Variants of Higher-Dimensional Automata
Level: M2
Contact: Uli Fahrenberg (uli@lmf.cnrs.fr)
Location: Laboratoire Méthodes Formelles, ENS Paris-Saclay
Keywords: Higher-dimensional automata; concurrency theory; automata theory
Description
Higher-dimensional automata (HDAs) are an extension of automata which allows to model concurrent and parallel executions. Like standard automata they consist of states and transitions, but also of higher-dimensional cells (squares, cubes, etc.) which model parallel execution of several events. This gives HDAs a somewhat geometric flavor.
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.
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.).
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
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.).
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.
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
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 :
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.
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.
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.
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.
::