Postes Ouverts
Internship Offers
Faithful Nash equilibria in games over graphs
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: Games of perfect information, Nash equilibria
Graphical Language for Clifford Hermiticians in Quantum Computing
Level: M1 - M2
Contact: Renaud Vilmart email: vilmart [at] lsv [dot] fr
Location: Laboratoire Méthodes Formelles, Université Paris-Saclay
Keywords: Quantum Computing, Graphical Language, Completeness, Hermitian Operators
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
Génération de simulations automobile à partir d’un modèle formel
Contact: Burkhart Wolff
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
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.
::