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. n 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.