Careers > Prove the robustness and functionality of critical units of the SPARK standard library
Last modified 10/20/2020 7:33:38 AM

Prove the robustness and functionality of critical units of the SPARK standard library

Internship
AdaCore
Paris, France
BAC +4/5

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.

Prove the robustness and functionality of critical units of the SPARK standard library

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 prove the correctness of critical parts of the SPARK standard library: primarily the units that manipulate characters and strings; then the runtime units that are used by the compiler to implement fixed-point arithmetic. The student will need to use the SPARK proof tools to demonstrate that no execution of these units can raise an exception (aka absence of runtime errors). The student will then add suitable contracts to these units that express the intended functionality as documented in the Ada Reference Manual, and use the SPARK proof tools to demonstrate that the implementation of the units respect these contracts. An initial source of inspiration for the expected results is the work done around “SPARK by Example” by a team at ISAE-SUPAERO (see https://github.com/tofgarion/spark-by-example). More complex programs such as an implementation of algorithm D by Knuth for multi-place division will require advanced use of the proof tools, with ghost code and unbounded arithmetic (see e.g. a blog post presenting such techniques at https://blog.adacore.com/using-spark-to-prove-255-bit-integer-arithmetic-from-curve25519).

 

Skills required: The work will require good understanding of program semantics, as well as capabilities in proving properties over programs.

Timeframe and location: 

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

 

Powered by Hello Talent