Internship Offers

Introduction of Timing Aspects into Event-B

Level: PhD

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...

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.

::