Two PhD student positions in verification, Paris (France)

Two PhD positions are available in the "Verification" team in LIAFA, Paris.

The first PhD position is on 'Software verification', specifically concurrent programs verification. Programs present several complex features that make their analysis very complex: concurrency, synchronisation, recursion, procedure calls, pointers, manipulation of integer and real variables, etc. Thus, the objective of this thesis is to investigate and develop new techniques, algorithms and tools for software analysis and model-checking that can deal with all these complex features.

The second PhD position is on 'Model-checking for malware detection'. Emulation based detection techniques for malware can only check the program's behavior in a limited time interval, whereas signature based systems are easy to get around. To sidestep these limitations, virus detectors need to use analysis techniques that check the behavior of the program in a static way, i.e. without executing it. The object of this thesis is to develop such new model-checking and static analysis techniques for virus detection.

The positions are available immediately. Candidates must have a master in computer science. The candidate must send a CV, university grades, recommendation letters, and a motivation letter to Tayssir Touili (touili at liafa.univ-paris-diderot.fr).

For more information, see the LIAFA site at http://www.liafa.univ-paris-diderot.fr/index_en.php or the webpage of Tayssir TOUILI at http://www.liafa.jussieu.fr/%7Etouili/.