3 ms·
> In fact, GenodeOS, seL4 and NVidia Autonomous Vehicle project are all using Ada/SPARK to some extent, As far as I am aware, seL4 does not use Ada/SPARK, but
by q-big 6y ago
> In fact, GenodeOS, seL4 and NVidia Autonomous Vehicle project are all using Ada/SPARK to some extent,
As far as I am aware, seL4 does not use Ada/SPARK, but C (with some assembler snippets), and Isabelle/HOL (for the proofs). This is also what is written in https://wwwnipkow.in.tum.de/teaching/proof21/SS18/files/14-final.pdf https://wwwnipkow.in.tum.de/teaching/proof21/SS18/files/14-f...
- pjmlp 6y agoMy mistake, I thought that Componolit work was for seL4, but it is also for Genode. https://componolit.com/index_en.html#components https://componolit.com/index_en.html#components