<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>