[isabelle] seL4 specification released



It took some time, but NICTA and Open Kernel Labs have now released the formal Isabelle/HOL specification of the seL4 microkernel. The C code of the kernel is verified (in Isabelle) to implement this specification. The release includes ARM and x86 binaries of the kernel, documentation, user-level libraries and examples, and a paravirtualised Linux that runs on top of seL4/x86:

http://ertos.nicta.com.au/software/seL4/

The specification works with Isabelle2009-2, and the release contains all files and libraries necessary to process it in Isabelle.

Please note that the release is for non-commercial only. Educational and academic research use is explicitly allowed. 

Cheers,
Gerwin






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.