Faculty Positions

Deux postes d'enseignants-chercheurs à l'ENS Paris-Saclay

Un poste de MCF et un poste de PU à l'ENS Paris-Saclay sont ouverts dans le DER Informatique et au Laboratoire Méthodes Formelles (LMF). Read more...

Deux postes d'enseignants-chercheurs à l'ENS Paris-Saclay

Un poste de MCF et un poste de PU à l'ENS Paris-Saclay sont ouverts dans le département d'informatique et au laboratoire LMF. Read more...

A Junior Professor position in Quantum Information at LMF

Université Paris-Saclay is about to open a Junior Professor position in Quantum Information with

The delays will be short, so here is a first informal announcement. Read more...

Un poste de professeur à Polytech, pour affectation au LMF ou au LISN

Un poste de professeur est ouvert au département informatique de Polytech Paris-Saclay, pour affectation au LMF ou au LISN.

Pour plus d'informations, veuillez prendre contact avec Frédéric Voisin, co-directeur du département d'informatique de Polytech et Patricia Bouyer-Decitre, directrice du LMF (pour une candidature au LMF).

Internship Offers

Term transformation and proof (re)construction

Find more details here.

Level: L3-M2

Supervisor: Frédéric Blanqui and Gabriel Hondet

Place: Deducteam, Laboratoire Méthodes Formelles (LMF), ENS Paris-Saclay, 4 avenue des Sciences, Gif-sur-Yvette, France.

Read more...

Translating Lean to Dedukti

Find more details here.

Level: M1-M2

Supervisor: Frédéric Blanqui and Floris van Doorn

Place: Deducteam, Laboratoire Méthodes Formelles (LMF), ENS Paris-Saclay, 4 avenue des Sciences, Gif-sur-Yvette, and Mathematics Department, University Paris-Saclay, bâtiment 307, rue Michel Magat, Orsay (there are 2.7 km between the two places)

Context: This internship is about formal proofs as digital objects, more specifically the translation of formal proofs between different proof systems. Read more...

Synchronization in Stochastic Games

Level: M2

Contact: Laurent Doyen

Keywords: automata theory, probability, algorithms.

Read the internship proposal in pdf.

Description

Finite-state stochastic games combine the stochastic aspects of Markov chains and the interactive aspects of two-player games. In a traditional view, Markov chains generate a probability measure over sequences of states (called paths), and questions such as “What is the probability that a path reaches a given state?” can be solved. In a more recent view, Markov chains generate a sequence of probability distributions {$d_i:Q \to [0,1]$} over their state space {$Q$} , where {$d_i(q)$} is the probability that the Markov chain is in state {$q \in Q$} after {$i$} execution steps. This distribution-based view has been considered recently in works on Markov chains and Markov decision processes (MDPs) [3, 1, 2], as a model of large- population systems consisting of several copies of the same process (molecules, sensors, bacteria, etc.). The dynamics of the system is described by a finite-state stochastic process, and a distribution {$d_i(q)$} is interpreted as the percentage of the population that is in state {$q$} at step {$i$}.

In this context, synchronization properties require that the sequence of probability distributions tends to accumulate all the probability mass in a given set {$T \subseteq Q$} of target states, that is all process instances synchronize in {$T$} . They generalize synchronizing properties of finite automata [4]. Different modes of synchronization can be defined, which require for instance the synchronization to occur once, or infinitely often. The synchronization modes are reminiscent of the traditional reachability, safety, Büchi, and coBüchi objectives [2].

In this internship (with possible continuation as a phd thesis), we consider stochastic games in the distribution-based view. We are looking for algorithmic solutions and structural properties of stochastic games where the objective of one of the player is given by a synchronization property. Several theoretical questions can be investigated and the solutions and heuristics can possibly lead to prototype implementations.

References

[1] S. Akshay, B. Genest, and N. Vyas. Distribution-based objectives for Markov decision processes. In Proc. of LICS: Logic in Computer Science, pages 36–45. ACM, 2018.

[2] L. Doyen, T. Massart, and M. Shirmohammadi. The complexity of synchronizing Markov decision processes. Journal of Computer and System Sciences, 100:96–129, 2019.

[3] V. A. Korthikanti, M. Viswanathan, G. Agha, and Y. Kwon. Reasoning about MDPs as transformers of probability distributions. In Proc. of QEST: Quantitative Evaluation of Systems, pages 199–208. IEEE Computer Society, 2010.

[4] M. V. Volkov. Synchronizing automata and the ˇCern ́y conjecture. In Proc. of LATA: Language and Automata Theory and Applications, LNCS 5196, pages 11–27. Springer, 2008.

Profile

  • Knowledge in automata theory, combinatorics, probabilities, and algorithms.
  • Language: French or English.

Where:

Laboratoire Méthodes Formelles (LMF)
École Normale Supérieure Paris-Saclay
4, avenue des sciences
91190 Gif-sur-Yvette
FRANCE

A HOL-CSP Case-Study : Analysing the Plain-Old-Telephone Protocol

Level: M1,M2

Contact: Burkhart Wolff, Safouan Taha

Summary. The theory of Communicating Sequential Processes going back to Hoare and Roscoe is still today one of the reference theories for concurrent specification and computing. This theory has been presented in Isabelle/HOL based on the denotational semantics of the Failure/Divergence Model of CSP; the resulting theory is called HOL-CSP. The "Plain Old Telephone Service" is a standard medium-size example for architectural modeling of a concurrent system. The goal of this internship is a formal analysis of deadlock and life lock properties of this protocol via interactive proof in Isabelle/HOL and Isabelle/HOL-CSP. Read more...

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.

Génération de simulations d'automobiles autonomes à partir d’un modèle formel

Niveau: M2, Postdoc

Contact: Burkhart Wolff

Lire la description du stage en pdf.

Contexte

Au sein de l’Institut de Recherche Technologique SystemX, situé au cœur du campus scientifique d’excellence mondiale de Paris-Saclay, vous prendrez une part active au développement d’un centre de recherche technologique de niveau international dans le domaine de l’ingénierie numérique des systèmes. Adossé aux meilleurs organismes de recherche français du domaine et constitué par des équipes mixtes d’industriels et d’académiques, ce centre a pour mission de générer de nouvelles connaissances et solutions technologiques en s’appuyant sur les percées de l’ingénierie numérique et de diffuser ses compétences dans tous les secteurs économiques.

Vous serez encadré par un ingénieur chercheur SystemX du domaine Sûreté de Fonctionnement, et vous aurez des échanges avec des chercheurs du Laboratoire Méthodes Formelles (LMF), notamment B. Wolff et S. Taha.

Vous travaillerez au sein du projet de recherche SystemX 3SA – Simulation pour la Sécurité des systèmes du véhicule Autonome – dont les partenaires industriels sont Apsys, AVsimulation, Expleo, Stellantis, Oktal-SE, Renault, SECTOR Group, Valeo et les partenaires académiques le CEA (Commissariat à l’Energie Atomique), le LNE (Laboratoire national de métrologie et d'essais) et le LMF (Laboratoire Méthodes Formelles).

Le poste est basé à l’IRT SystemX – 2, Boulevard Thomas Gobert 91120 Palaiseau.

Durée et date de démarrage

Durée du stage : 6 mois
Date de démarrage envisagée : février 2022

Read more...

Génération de simulations automobile à partir d’un modèle formel

Contact: Burkhart Wolff

Description du stage en pdf.

Contexte

Au sein de l’Institut de Recherche Technologique SystemX, situé au cœur du campus scientifique d’excellence mondiale de Paris-Saclay, vous prendrez une part active au développement d’un centre de recherche technologique de niveau international dans le domaine de l’ingénierie numérique des systèmes. Adossé aux meilleurs organismes de recherche français du domaine et constitué par des équipes mixtes d’industriels et d’académiques, ce centre a pour mission de générer de nouvelles connaissances et solutions technologiques en s’appuyant sur les percées de l’ingénierie numérique et de diffuser ses compétences dans tous les secteurs économiques.

Vous serez encadré par un ingénieur chercheur SystemX du domaine Sûreté de Fonctionnement, et vous aurez des échanges avec des chercheurs du Laboratoire Méthodes Formelles (LMF), notamment B. Wolff et S. Taha.

Vous travaillerez au sein du projet de recherche SystemX 3SA – Simulation pour la Sécurité des systèmes du véhicule Autonome – dont les partenaires industriels sont Apsys, AVsimulation, Expleo, Stellantis, Oktal-SE, Renault, SECTOR Group, Valeo et les partenaires académiques le CEA (Commissariat à l’Energie Atomique), le LNE (Laboratoire national de métrologie et d'essais) et le LMF (Laboratoire Méthodes Formelles).

Le poste est basé à l’IRT SystemX – 2, Boulevard Thomas Gobert 91120 Palaiseau.

Durée et date de démarrage

Durée du stage : 6 mois
Date de démarrage envisagée : février 2022

Read more...

Quantum networks theory

Contact: Pablo Arrighi

Follow this link for a PDF with a complete description of the topic.

Quantum Networks Theory

Level: M2

Contact: Pablo Arrighi

Read the complete description of the internship topic in PDF.

Deciding the Logic of Subsequences

Level: M2

Contact: Philippe Schnoebelen

The logic of subsequences is the logic of the structure {$(X^*;\leq_*,..)$} where the universe {$X^*$} contains all finite sequences over some base set {$X$}, and where {$\leq_*$} is the subsequence relation (as in Higman's Lemma).

For example, this logic allows writing constraints like {$$ \tag{$\phi$} {aa}\leq_* x \land {bb}\leq_* x \land {ab}\not\leq_* x $$} where {$a,b$} are letters and {$x$} is a variable standing for an unknown word. Over {$X=\{a,b\}$}, the two-letter alphabet, the solution set of the above constraint is the language {$L_\phi={bbb}^*{aaa}^*$}.

The logic allows more complex formulae, like

\begin{equation*} \tag{$\psi$} \forall x,y: \exists z: \bigl( x\leq_* z\land y\leq_* z \land \forall u: x\leq_* u\land y\leq_* u\implies z\leq_* u \bigr) \end{equation*} that states that {$(X^*,\leq_*)$} is an upper semilattice. Whether {$\psi$} is true or false depends on {$X$}.

The goal of this Master Internship is to develop the computational theory of the logic of subsequences, especially by identifying decidable fragments of the logic and assessing their algorithmic complexity.

Read more...

::