About the role
Formal verification of device drivers on the Raspberry Pi Pico using SPARK Careers > Formal verification of device drivers on the Raspberry Pi Pico using SPARK Last modified 10/10/2022 1:20:51 PM Formal verification of device drivers on the Raspberry Pi Pico using SPARK Internship AdaCore Paris, 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: The Raspberry Pi Pico is a small and cheap board that can be used to develop a wide range of embedded applications. Recently, it has become possible to program the Pico using Ada thanks to the rp2040_hal project, a library of device drivers written entirely in Ada. Such low-level code poses interesting challenges for formal verification tools such as SPARK, and this is why most of the existing code is not written in SPARK, but in Ada. The objective of this internship is to explore the possibility of programming the Pico in SPARK, possibly modifying existing libraries to make them more compatible with SPARK. Another candidate library for this work is the “usb_embedded” library, a USB device stack currently implemented in Ada. Skills required: - good programming skills - experience with low-level programming - willingness to learn new skills, such as formal verification Timeframe: During 2023 - 6 months Powered by