Faculty Positions

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

Read more...

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

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

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.

Connecting Isabelle/HOL-CSP with FDR4

Level: L3

Contact: Burkhart Wolff

Summary.HOL-CSP is a powerful proof-environment based on Isabelle/HOL and the process algebra 'Communicating Sequential Processes' developed by Tony Hoare and Bill Roscoe in the 90ies. In particular, HOL-CSP can model and reason over processes with infinite event structures, so dense time, physical states, algebraic structures, .... Intro FDR4 is a model-checker that provides automated proofs for process-refinements for finite event structures. It is a research question if and to what extent HOL-CSP can be combined with FDR4.

As a prerequisite, the internal presentation of FDR4, a so-called "Labelled Transition System" (LTS) representing CSP processes must be converted into a JSON format that can be read by Isabelle. For this purpose, an internal FDR4 API must be extended by functions that convert the internal LTS data-structure into a JSON output file.

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

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

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

Quantum networks theory

Contact: Pablo Arrighi

Follow this link for a PDF with a complete description of the topic.

::