[TYPES/announce] PhD position in machine learning for formal verification (Université Paris-Saclay, CEA LIST Institute, France)

[Michele Alberti]

Dear all,

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.

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.

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.

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.

Knowledge in the following fields is required:

- Machine learning or deep learning
- Python programming

Some knowledge in program verification is especially welcome.

A full description of the position is available online: 
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$ 

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.

For further information and inquiries, please contact:

  * Michele Alberti (michele.alberti at cea.fr)
  * Valentin Perrelle (valentin.perrelle at cea.fr)

Best regards,

Michele Alberti
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-announce/attachments/20220329/652585b4/attachment-0001.htm>