> Academic opportunities > PHD positions

Machine learning for improving formal verification of code

Technological challenge: Artificial intelligence & Data intelligence (learn more)

Department: Département Ingénierie Logiciels et Systèmes (LIST)

Laboratory: Laboratoire pour la Sûreté du Logiciel

Start Date: 01-09-2022

Location: Saclay

CEA Code: SL-DRT-22-0590

Contact: michele.alberti@cea.fr

Frama-C, developed in our laboratory, is a C program analysis platform that provides several collaborative analyzers in the form of plug-ins. Frama-C allows the user to annotate C programs with formal specifications written in the ACSL language and to combine its analyzers to verify them, in particular the Eva and WP plugins. Both provide highly customizable techniques that require fine-grained expertise for effective use. Moreover, many of these techniques are more or less based on heuristics and strategies that are usually designed manually. They are often suboptimal, fragile, and require considerable technical knowledge and effort to design. As such, they do not generalize or adapt well to different code bases, and must be updated over time. The goal of this thesis is to integrate machine learning approaches to the Frama-C static analyzers in order to improve their usability and scalability. The thesis will start by studying which heuristics already in place in Eva or WP could be learned automatically. Then, the PhD student will study the representations and learning algorithms best suited for treating code. The PhD student will propose and implement a machine learning pipeline for code verification strategies. Furthermore, the PhD student will integrate such strategies into Frama-C and evaluate their performance with respect to those already in place today.

See all positions Download the offer (.zip)

Email Bookmark and Share