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 ([email protected]) and Didier
Lime ([email protected]). Please feel free to ask more details
about the project, the salaries, and the research environment.
--
--------------------------------------------
--------------------------------------------
Benoît Delahaye
Maître de Conférences
Responsable du M1 MIAGE
Responsable "Taxe d'Apprentissage"
Université de Nantes/LINA
+33 (0)2 51 12 58 45
----
[[ Petri Nets World: ]]
[[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/ ]]
[[ Mailing list FAQ: ]]
[[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/pnml/faq.html ]]
[[ Post messages/summary of replies: ]]
[[ [email protected] ]]
