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

Read more...

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

Read more...

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

Read more...

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

Read more...

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

Read more...

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

Read more...

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

Read more...

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

Read more...

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

Read more...

Synchronization in Stochastic Games

Level: M2

Contact: Laurent Doyen

Keywords: automata theory, probability, algorithms.

Read more...

::