LIPN lab hiring an associated professor on formal verification

General profile: Computer Science

Job profile: Formal verification


The Computer Science department of Institut Galilée contributes in different curricula of the institute: Bachelor, Master, graduate school, Sup’Galilée engineering school. The recruited person will be part of the Computer Science department. S/he will give lectures in different areas of computer science at all levels and curricula, in particular in the basic courses.

The department seeks lecturers in many domains, more specifically in software engineering, computer systems, and object-oriented programming. The ability to deliver courses in these specific areas will be appreciated. It will also be possible to lecture at the Master level in the formal specification and verification domain. The recruited person is expected to get involved in the department duties through pedagogic responsibilities such as course responsibility, year of studies management, or students’ tutoring.

The law on Orienteering and Success of Students (Orientation et Réussite des Étudiants – ORE) financially supports the increase of the number of students. In that context teaching is in Bachelor and mainly in first year of studies.

Department and area: Institut Galilée – Computer science

Location: Villetaneuse Campus – Université Sorbonne Paris Nord


Head of computer science department: Kaïs Klai


Paris North Computer Science Laboratory (Laboratoire d’Informatique de Paris-Nord – LIPN, CNRS UMR 7030) wants to strengthen the Verification axis of the LoVe team by recruiting an associate professor.

The research of the Verification axis addresses formal verification of models for safety and security of systems. Various formal models are considered (Petri nets, timed automata, parametric automata, pushdown automata, …) as well as logics for expressing their properties (LTL, CTL, TCTL, ATL, …), thus taking into account several perspectives for the systems studied. These various models raise both theoretical and practical challenges, their formal verification is complex (the higher their analysis capabilities, the lower their expressive power). The team research works aims at pushing the limits of model checking with several complementary new approaches to state space reduction (symbolic structures, modularity, partial orders parallelization, ).

Adapting and applying the proposed approaches to specific domains (distributed algorithms, network protocols, virus detection, security, business processes, resource management in the cloud, diagnostic,) is also a major objective. Taking into account the intrinsic characteristics of these domains allows for designing dedicated verification approaches, that are more efficient than the regular ones. The complementarity of the team members expertise is a key to achieves these goals.

The developed approaches are implemented in several tools and platforms (IMITATOR, SMODIC, STAMAD, CosyVerif, Helena, PMCSOG) which allow for evaluating the adequacy and efficiency of the results for case studies or benchmarks and give the team additional visibility on the international scene.

The expertise of the recruited person and her/his research project must be integrated withing the team research works. Teamwork on the scientific topics is expected from the recruited person for short and long term.

Location : Villetaneuse campus

Laboratory: Laboratoire d’Informatique de Paris Nord (LIPN) – CNRS UMR 7030

Contact :

Director of LIPN: Frédérique Bassino