[FM-India] PhD position on formal verification at Université Paris 13 / École Centrale Nantes (France)

Madhavan Mukund madhavan at cmi.ac.in
Wed Jan 27 19:53:29 IST 2016

 Date: Wed, 27 Jan 2016 13:58:33 +0100
 From: Étienne André <Etienne.Andre at lipn.fr>
 To: fmindia at cmi.ac.in
 Subject: PhD position on formal verification at Université Paris 13 / École Centrale Nantes (France)
                         PhD position                       
  Title       : Formal verification of parametric real-time systems with preemption
  Laboratory 1: LIPN, CNRS UMR 7030, Université Paris 13, Sorbonne Paris Cité, France
  Laboratory 2: IRCCyN, École Centrale Nantes, France
  Contact     : Étienne André and Didier Lime
                application.phd.pacs at lipn.univ-paris13.fr
 *** Full subject available at
  Context of the subject
 Real-time systems have become ubiquitous in the past few years.
 Some of them (automated plane and unmanned systems control, banking
 systems, etc.) are critical in the sense that no error must occur.
 Testing these systems can possibly detect the presence of bugs, but not
 guarantee their absence.
 It is thus necessary to use formal methods such as model checking so as
 to  formally prove their correctness.
 Real-time systems are characterized by a set of timing constants, such
 as the reading period of a sensor on an unmanned aircraft system, the
 traversal time of a circuit by the electric current, or the delay before
 retransmitting data in a cellphone.
 Although numerous techniques to verify a system for one set of constants
 exist, formally verifying the system for numerous values of these
 constants can require a very long time, or even infinite if one aims at
 verifying dense sets of values.
 It is therefore interesting to use parameterized techniques, by
 considering that these constants are unknown, i.e. parameters, and
 synthesize a constraint on these parameters guaranteeing the system
 Parametric timed automata have been proposed to model and verify
 parametric timed systems, and tools such as Romeo and IMITATOR were
 developed to perform efficient analyses.
 This formalism extends finite state automata with clocks (real-valued
 variables) that are compared with parameters in linear inequalities.
 Parameter synthesis can also be used to study the "implementability" of
 a system, i.e. its robustness w.r.t. infinitesimal variations of the
 timing constants.
 The goal of this PhD is to:
 1) study parameter synthesis for parametric timed automata and hybrid
 2) devise efficient algorithms reusing recent concepts such as the
 integer hulls;
 3) implement all algorithms in state-of-the art tools.
 Formal methods, model checking, real-time systems, parameter synthesis
 One or several of the following skills would be appreciated (though not
     - formal methods;
     - model checking;
     - (parametric) timed automata, (parametric / timed) Petri nets;
     - C++ or OCaml programming.
  Context: The PACS Project
 This post-doctoral position is funded by national project ANR PACS
 (Parametric Analyses of Concurrent Systems) 2014--2019.
 ANR PACS involves four laboratories: LIPN (Paris 13), IRIF (Paris 7),
 IRCCyN (École Centrale Nantes) and LINA (Université de Nantes).
 In addition, Kim Larsen's group in Aalborg (Denmark) acts as a foreign
 LIPN is a high-quality laboratory involving about 80 professors,
 associate professors and full-time researchers, and many more students.
 Université Paris 13 is located less than 30 minutes from central Paris.
 IRCCyN is a leading laboratory in the domain of cyber-physical systems
 and robotics, with about a hundred researchers. It is located in Nantes,
 on the west coast of France, two hours from Paris by a direct,
 high-speed train.
  Conditions and Application
 The PhD position is for three years, and can start anytime (the sooner
 the better), and in any case before October 1st, 2016.
 The monthly salary is 1400€ + an additional 250€ if teaching 64h/year
 (netto, but before income tax, about 5,5%).
 Local transportation fees (Paris métro) are subsidized by half by the
 Applications shall be made by email to Didier Lime and Étienne André,
 enclosing a fully detailed curriculum, and any other relevant document
 (recommendations, etc.).
  Contact   : Étienne André and Didier Lime
              application.phd.pacs at lipn.univ-paris13.fr

More information about the FMIndia mailing list