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.
Internship Offers
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
Semantics of Boolean Networks
Level: M2
Contact: Philippe Dague <philippe.dague [at] universite-paris-saclay [dot] fr>, Thomas Chatain <thomas.chatain [at] ens-paris-saclay [dot] fr>
Location: Laboratoire Méthodes Formelles, Université Paris-Saclay
Keywords: Boolean Networks, update modes
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
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.
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.
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.).
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.).
Faithful Nash equilibria in games over graphs
Level: M1 - M2
Contact: Dietmar Berwanger (dwb@lsv.fr) and Patricia Bouyer (bouyer@lsv.fr)
Location: Laboratoire Méthodes Formelles, ENS Paris-Saclay
Keywords: Games of perfect information, Nash equilibria
Introduction of Timing Aspects into Event-B
Level: M2
Contact: Idir Ait Sadoune <idir.aitsadoune [at] centralesupelec [dot] fr>,
Location: Laboratoire Méthodes Formelles, Université Paris-Saclay
Keywords: Event B, Timed systems
Various subjects on proof system interoperability
Find more details here.
Supervisor: Frédéric Blanqui
Place: Deducteam, Laboratoire Méthodes Formelles (LMF), ENS Paris-Saclay, 4 avenue des Sciences, Gif-sur-Yvette
::