[FM-India] Two PhD positions in LIAFA, Paris, France: Software verification and Model-checking for malware detection

[Madhavan Mukund]

 ===============================
 
 Two PhD positions in LIAFA
 <http://www.liafa.univ-paris-diderot.fr/index_en.php>
 ==================
 
 Contact: Tayssir TOUILI <http://www.liafa.jussieu.fr/%7Etouili/>
 (touili at liafa.univ-paris-diderot.fr)
 
 Two PhD positions are  available in the "Verification" team in LIAFA, Paris.
 
 
 *Subject 1: Software  verification**
 **------------------------------------------*
 
 The subject of the thesis is about concurrent programs verification.
 The PhD student is expected to investigate and develop novel
 techniques, algorithms and tools for the analysis of software.
 
 Indeed, nowadays, software is everywhere: in telecommunication, in
 navigation, in nuclear plants, etc.

 The tasks that software deal with are becoming more and more complex
 and critical, in the sense that any small error can cause huge human
 and/or economical damages. Therefore, it is crucial to be sure that a
 software does not contain any error before using it.  Programmers
 need then to have rigorous formal mathematical techniques that allow
 to verify and check their programs.

 Unfortunately, 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 develop new
 techniques for software model-checking that can deal with all these
 complex features.
 
 *Subject 2: Model-checking for malware detection*
 *-----------------------------------------------------------------*
 
 The topic of the thesis is the development of new original
 model-checking and static analysis techniques for malware detection.
 Indeed, the number of malwares is growing extraordinarily fast.

 Therefore, it is important to have efficient malware detectors.  To
 identify viruses, existing antivirus systems use either code
 emulation or signature (pattern) detection.

 These techniques have some limitations. Indeed, emulation based
 techniques 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, instead of executing the program or
 making a syntactic check over it, virus detectors need to use
 analysis techniques that check the /*behavior*/ (not the syntax) of
 the program in a /*static*/ way, i.e.  without executing it.

 Towards this aim, we propose in this thesis to develop new
 /*model-checking*/ and /*static analysis */ techniques for virus
 detection.
 
 
 *How to apply:**
 **==========*

 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)

 ===============================