Elsa joined AdaCore in 2023 as an intern in the SPARK team as part of her engineering degree at ENSIIE.
2 entries written by Elsa Ferrara
Tetris was the first computer game played in space but let's review our ambitions for the time and try to implement it on a Raspberry Pico first. This idea appeared during my internship at AdaCore. The main purpose of my internship was to explore the possibilities of formal verification in device drivers using SPARK. It seemed both very challenging and valuable to prove such low-level code to ensure safety and security.
Programming device drivers requires certain practices or operations. These include, for example, the multitude of volatile variables in the code. On the other hand, SPARK imposes a number of restrictions on programs and also limits the use of certain practices permitted in Ada. Here's a list of hurdles I encountered during my internship involving driver code and the rules authorized by SPARK. I also present ways of getting around these problems, as well as some best practices for having the most SPARK-compatible code in advance. This list is not exhaustive.