Careers > Software Engineer - Improve user experience in GNATprove flow analysis output
Last modified 11/28/2022 9:50:48 AM

Software Engineer - Improve user experience in GNATprove flow analysis output

Internship
AdaCore
Toulouse, France
Bac +4/5

Everything we do at AdaCore is centered around helping developers build the safest, most secure open-source software. 

For over 25 years, we've worked with global leaders across avionics, aerospace and defense industries, building tools and providing services that ease the complex and difficult process of developing high-integrity software. As the need for truly secure and reliable applications expands into industries such as automotive, medical, energy, and IOT, we’re advancing our time-tested technologies to bring expertise and services to help a whole new generation of developers.

Our 150 experts worldwide in the US (New York), France (Paris, Toulouse, Grenoble and Vannes), the UK, Estonia and Germany all play a role in developing bleeding edge technologies to meet the highest grade of software development.

Joining AdaCore is about joining a culture of innovation, openness, collaboration and dependability, which defines how we work together, with our customers and partners.

Context:

SPARK is a subset of the Ada programming language, together with formal verification tools which allow giving mathematical guarantees about SPARK programs, from correct data flows to absence of runtime errors to correct implementation of functional requirements. SPARK is open source and freely available to the Community on Alire, a package manager for Ada, as well as professionally supported by AdaCore, which co-develops SPARK with Inria.

Goal:

When running GNATprove, the formal verification tool for SPARK, the user code is analysed for data flow errors and then proved for correctness. The goal of this internship is to improve the user experience with the results of flow analysis, as proving the code requires frequent interactions with the user, which depends on the tool issuing rich and precise messages.

The following working report group (http://web.eecs.umich.edu/~akamil/papers/iticse19.pdf), suggests guidelines to follow when trying to improve the error reporting on a compiler. Those can be adapted to match the needs for flow analysis reporting.

As a first step, the existing flow analysis output could be refined by grouping messages together, adding diagnoses and explanations, such as the work done for rustc (see https://www.youtube.com/watch?v=Z6X7Ada0ugE&t=1058s). The student will also work on the addition of extra information on messages to better integrate the tool in IDEs. 

This can include the implementation of code fixes, available with a simple click, as well as the addition of explanations in comments to help the user understand the checks.

Additionally, some work has already been done in the proof part of the tool to guide the user into proving their code (see https://www.adacore.com/papers/how-the-analyzer-can-help-the-user-help-the-analyzer). Other heuristics for the proof or flow analysis tools could be implemented as part of this internship.

Skills required:

- good understanding of program semantics

- good programming skills

- interest in user experience

- knowledge of graph theory (optional)

Timeframe:

During 2023 - 6 months

Powered by Hello Talent