Postdoc Position(s) in Formal Methods for parametric quantitative systems

Two 1-year postdoc positions (or potentially one 2-year) are available at LINA/IRCCYN (wich will become LS2N in 2017) in Nantes, funded by the French ANR project PACS (Parametric Analyses of Concurrent Systems -- http://lipn.univ-paris13.fr/PACS/).

** PROJECT **

Model-checking and formal modeling are now techniques with a certain recognition, but their applicability in practice remain somewhat inferior to expectations. This is in part due to two main problems:
rather rigid modeling of the systems impairing abstraction and scalability, and insufficient feedback from the verification process. In the PACS project, we address these issues by lifting these techniques to the more flexible and rich setting of parametrised formal models.

In that setting, some features of the system like the number of processes, the size of some buffers, communication delays, deadlines, energy consumption, and so on, may be not numerical constants, but rather unknown parameters. The model-checking questions then become more
interesting: is some property true for all values of the parameters? Or does there exist some value such that it is? Or even what are all the possible values such that it is?

The candidates will work on the topic of parameter synthesis / parametric verification with a particular focus on probabilistic and/or timed systems. This involves the development of new formalisms, their theoretical study, as well as the design of new algorithms and tools implementing them to extend the applicability of parameters in formal methods.

Successfull candidates will join the "AeLoS" team at LINA and/or the "STR" team at IRCCYN, to work with Benoit Delahaye, Didier Lime, and Olivier H. Roux.

** CANDIDATES **

• We seek candidates with a strong background in Computer Science with an interest in formal methods, programming languages, and algorithms.
• Experience in timed/probabilistic systems would be advantageous.
• Applicants should have a strong theoretical background, but also some minimal experience with software development. Candidates should provide evidence of relevant work, where possible, and must demonstrate a desire to perform internationally-leading research.

** APPLICATION **

Interested candidates should send a short motivation letter, alongside other supporting documents like the CV and the names of two reference persons, to Benoit Delahaye (benoit.delahaye@univ-nantes.fr) and Didier Lime (didier.lime@ec-nantes.fr). Please feel free to ask more details about the project, the salaries, and the research environment.