Replies: 1 comment
-
|
There's probably a good number of papers on this subject. A good place to start looking is anything related to seL4? |
Beta Was this translation helpful? Give feedback.
0 replies
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
-
Something that would interesting to try would be to formally verify some core parts of the OS, ie, proving the IPC mechanisms are correct, and for some critical compontents, proving that all invariants are maintained.
It would be nice to do this for, ie, the slab allocator, so we can safely ignore the warnings that are present right now.
Beta Was this translation helpful? Give feedback.
All reactions