<html>
<head>
<meta http-equiv="content-type" content="text/html;
charset=ISO-8859-1">
</head>
<body bgcolor="#FFFFFF" text="#000000">
Please distribute (apologies for multiple postings): <br>
<br>
===============================<br>
<br>
Two PhD positions in <a
href="http://www.liafa.univ-paris-diderot.fr/index_en.php">LIAFA</a><a
rel="nofollow" target="_blank"><span class="yshortcuts"
id="lw_1248182257_0"></span></a><br>
==================<br>
<br>
Contact: <a rel="nofollow" target="_blank"
href="http://www.liafa.jussieu.fr/%7Etouili/"><span
class="yshortcuts" id="lw_1248182257_1">Tayssir TOUILI</span></a>
(<a rel="nofollow" class="moz-txt-link-abbreviated"
ymailto="mailto:touili@liafa.jussieu.fr" target="_blank"
href="http://us.mc502.mail.yahoo.com/mc/compose?to=touili@liafa.jussieu.fr"><span
class="yshortcuts" id="lw_1248182257_2">touili@liafa.univ-paris-diderot.fr</span></a>)<br>
<br>
Two PhD positions are available in the "Verification" team in
LIAFA, <span class="yshortcuts" id="lw_1248182257_3">Paris</span>.
<br>
<br>
<br>
<b>Subject 1: Software verification</b><b><br>
</b><b>------------------------------------------</b><br>
<br>
The subject of the thesis is about concurrent programs
verification.<br>
The PhD student is expected to investigate and develop novel
techniques, algorithms and tools for<br>
the analysis of software.<br>
<br>
Indeed, nowadays, software is everywhere: in telecommunication, in
navigation, in nuclear plants, etc. <br>
The tasks that software deal with are becoming more and more
complex and critical, in the sense that any <br>
small error can cause huge human and/or economical damages.
Therefore, it is crucial to be sure that <br>
a software does not contain any error before using it. Programmers
need then to have rigorous <br>
formal mathematical techniques that allow to verify and check their
programs.<br>
Unfortunately, programs present several complex features that make
their analysis very complex: <br>
concurrency, synchronisation, recursion, procedure calls, pointers,
manipulation of integer and real variables, etc.<br>
Thus, the objective of this thesis is to develop new techniques for
software model-checking that can deal with all these complex
features.<br>
<br>
<br>
<br>
<br>
<b>Subject 2: Model-checking for malware detection</b><br>
<b>-----------------------------------------------------------------</b><br>
<br>
The topic of the thesis is the development of new original
model-checking and static analysis <br>
techniques for malware detection. Indeed, the number of malwares
is growing extraordinarily fast. <br>
Therefore, it is important to have efficient malware detectors.<br>
To identify viruses, existing antivirus systems use either code
emulation or signature (pattern) detection.<br>
These techniques have some limitations. Indeed, emulation based
techniques can only check the<br>
program's behavior in a limited time interval, whereas signature
based systems are easy to get around. <br>
To sidestep these limitations, instead of executing the program or
making a syntactic check over it,<br>
virus detectors need to use analysis techniques that check the <i><b>behavior</b></i>
(not the syntax) of the program in a <i><b>static</b></i> way,
i.e. without executing it.<br>
Towards this aim, we propose in this thesis to develop new <i><b>model-checking</b></i>
and <i><b>static analysis </b></i> techniques for virus detection.<br>
<br>
<span id="result_box" class="" lang="en"><span class="hps"><br>
</span></span><b>How to apply:</b><b><br>
</b><b> ==========</b><br>
The positions are available immediately. Candidates must have a
master in <span style="background: transparent none repeat scroll 0%
50%; cursor: pointer; -moz-background-clip: -moz-initial;
-moz-background-origin: -moz-initial;
-moz-background-inline-policy: -moz-initial;" class="yshortcuts"
id="lw_1248182257_5"> computer science</span>.<br>
The candidate must send a CV, university grades, <span
style="background: transparent none repeat scroll 0% 50%; cursor:
pointer; -moz-background-clip: -moz-initial;
-moz-background-origin: -moz-initial;
-moz-background-inline-policy: -moz-initial;" class="yshortcuts"
id="lw_1248182257_6">recommendation letters</span>, and a
motivation letter to Tayssir TOUILI (<a rel="nofollow"
class="moz-txt-link-abbreviated"
ymailto="mailto:touili@liafa.jussieu.fr" target="_blank"
href="http://us.mc502.mail.yahoo.com/mc/compose?to=touili@liafa.jussieu.fr">touili@liafa.univ-paris-diderot.fr)</a>
</body>
</html>