seL4 in Australia: From Research to Real-World Trustworthy Systems
An overview of developments, and of ongoing research, related to the correctness proof of the seL4 microkernel.
June Andronick
Advertisement
Author Archives
Formally Verified Software in the Real World
Verified software secures the Unmanned Little Bird autonomous helicopter against mid-flight cyber attacks.
seL4: Formal Verification of an Operating-System Kernel
We report on the formal, machine-checked verification of the seL4 microkernel from an abstract specification down to its C implementation. We assume correctness of compiler, assembly code, hardware, and boot code.
Shape the Future of Computing
ACM encourages its members to take a direct hand in shaping the future of the association. There are more ways than ever to get involved.
Get Involved