Careers > Validate prover counterexamples through concrete simulation for SPARK
Last modified 9/28/2021 10:06:12 AM

Validate prover counterexamples through concrete simulation for SPARK

Internship
AdaCore
Paris
Bac + 4/5

AdaCore: Helping Developers Build Software that Matters

Everything we do at AdaCore is centered around helping developers build safe, secure and reliable software.

For over 25 years, we've worked with global leaders across the military and civil avionics, defense systems, air traffic management/control, space, railway, and financial services 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. Through our subscription-based business model and dedicated services arm, we have worked with hundreds of customers over the year on thousands of projects.

Our 120 experts worldwide in the US (New York, Lexington), France (Paris, Toulouse, Grenoble and Vannes), the UK, and Estonia, all play a role in developing state-of-the-art technologies to meet the challenges of building the highest grade of software.

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

 

Validate prover counterexamples through concrete simulation for SPARK

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 www.adacore.com/download as well as professionally supported by AdaCore, which co-develops SPARK with Altran and Inria. 

Goal:

The subject of this internship is to validate the counterexamples generated by the automatic prover CVC4 (although another prover could be used too, like Z3) when it cannot prove a given Verification Condition produced by the SPARK tool. AdaCore and Inria have been working together on counterexamples for the joint technologies SPARK and Why3 since 2015, with major advances in their usability and usefulness (see related articles on https://www.adacore.com/proofinuse). Recently, work has focused on validating counterexamples generated by provers through the use of simulation of the execution of the counterexample with two related semantics: https://cister-labs.pt/f-ide2021/images/preprints/F-IDE_2021_paper_6.pdf 

 

This work has allowed us to remove all cases where counterexamples do not correspond to a possible concrete execution. But due to the current limitations of the concrete simulation engine, it also removes cases where valid counterexamples are not recognized as such. Also, the benefits of the dual semantics to alert users on missing contracts for proof are not fully exploited yet. These have the potential to drastically increase the benefits of counterexamples for users. The ability to generate a “proof of concept” of errors by the SPARK tool is highly valued by users (see this recent talk by NVIDIA security researchers: https://youtu.be/iz_Y1lOtX08?t=892), but it still falls short of providing all the expected benefits on more complex programs. The goal of this internship is to improve that.

 

Skills required: very good development skills, good understanding of program semantics

 

Timeframe and location:

 

The internship will take place in the offices of AdaCore in Paris. 

Powered by Hello Talent