<html>
<head>
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
</head>
<body>
Dear all,<br>
<br>
The Software Reliability and Security Lab at CEA LIST (Université
Paris-Saclay, France) is hiring a PhD student (3 years contract) to
work on machine learning for formal software verification in the
context of Frama-C.<br>
<br>
Frama-C is an open-source platform providing several analyzers for C
code as plug-ins. The most notables are Eva, based on abstract
interpretation, and WP, based on the weakest preconditions calculus.<br>
<br>
Both plug-ins provide highly parametrizable techniques that may be
efficiently combined, but their activation may be prohibitive in
terms of resources such as time of computation and memory footprint.
Moreover, many of these techniques are more or less based on
heuristics which are usually manually conceived. These heuristics
may be suboptimal, and require considerable technical knowledge and
effort to be devised.<br>
<br>
The goal of the PhD is to integrate machine learning approaches to
the Frama-C static analyzers in order to overcome the aforementioned
shortcomings. The PhD will start by studying which heuristics
already in place in Eva or WP could be automatically learned. Later,
the PhD will investigate and propose representations and learning
algorithms for treating code, with a particular focus on maintaining
as much as possible the semantic elements. The developed research
work will be evaluated on academic and industrial use cases.<br>
<br>
Knowledge in the following fields is required:<br>
<br>
- Machine learning or deep learning<br>
- Python programming<br>
<br>
Some knowledge in program verification is especially welcome.<br>
<br>
A full description of the position is available online: <a class="moz-txt-link-freetext" href="https://urldefense.com/v3/__https://www.frama-c.com/jobs/2022-03-28-machine-learning-for-improving-formal-verification-of-code.html__;!!IBzWLUs!Fm729NmlR-JkMcegkpifxE1F9cA302IV40lGZmGHsSYM_GbU5yObqVi3MRthnXUGcJ0XMO0ccDv3xA$" moz-do-not-send="true">https://www.frama-c.com/jobs/2022-03-28-machine-learning-for-improving-formal-verification-of-code.html</a><br>
<br>
The starting date is expected to be in September 2022. However, we
suggest the interested candidates to get in touch with us as soon as
possible as a 3+ month procedure for administrative and security
purposes is typically required by CEA.<br>
<br>
For further information and inquiries, please contact:<br>
<ul>
<li>Michele Alberti (<a class="moz-txt-link-abbreviated
moz-txt-link-freetext" href="mailto:michele.alberti@cea.fr"
moz-do-not-send="true">michele.alberti@cea.fr</a>)</li>
<li>Valentin Perrelle (<a class="moz-txt-link-abbreviated
moz-txt-link-freetext" href="mailto:valentin.perrelle@cea.fr"
moz-do-not-send="true">valentin.perrelle@cea.fr</a>)</li>
</ul>
<p>Best regards,</p>
Michele Alberti<br>
</body>
</html>