Formal proof in embedded systems part 1
During the last months, a lot of work has been done in the Sentry kernel in order to validate the absence of run time error, including all undefined behaviors, but also usual RTEs such as invalid memory access, out-of-bounds and integer algorithmic errors not being UB (overflow, downcast, etc.).
This work has been done with Frama-C framework, and works well even when targeting embedded kernel (typically targeting armv7-m and armv8-m).
We also cover low level parts such as drivers and hardware registers manipulations.
