AdaCore Blog

Elsa Ferrara

Elsa Ferrara

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

Formal Proof on Device Drivers with SPARK

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.