Faculty Positions
Un poste d'enseignant-chercheur à 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
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
Safety Analysis of Real-Time Discrete-Event and Hybrid Systems
Level: M2
Contact: Philippe Dague <philippe.dague [at] universite-paris-saclay [dot] fr>, Lina Ye <lina.ye [at] centralesupelec [dot] fr>
Location: Laboratoire Méthodes Formelles, Université Paris-Saclay
Keywords: Timed Automata, Hybrid Automata, Diagnosability, Approximations, CEGAR, SMT, PINN
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
The compositional structure of indefinite causal order
Level: M1 - M2
Contact: Augustin Vanrietvelde <augustin.vanrietvelde [at] inria [dot] fr>
Location: Laboratoire Méthodes Formelles, Université Paris-Saclay
Keywords: Quantum Information, indefinite causal order, causality, quantum circuits
Sectorial constaints in quantum physics
Level: M1 - M2
Contact: Augustin Vanrietvelde
Email: augustin.vanrietvelde [at] inria [dot] fr
Location: Laboratoire Méthodes Formelles, Université Paris-Saclay
Keywords: Quantum Information, Sectorial constraints, Quantum circuits
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
Synthesizing coalition strategies in parameterized concurrent games
Level: M1 - M2
Contact: Patricia Bouyer (bouyer@lsv.fr)
Location: Laboratoire Méthodes Formelles, ENS Paris-Saclay
Keywords: Parameterized verification, concurrent games, distributed computing, formal languages
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
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
::
