On Mon, May 25, 2015 at 12:09 AM, Gerwin Klein
Cool, will be nice to follow your progress there.
Minor nitpick: "seL4 is a new open-source L4 microkernel developed by General
Dynamics C4 Systems and NICTA”: seL4 was exclusively developed by NICTA, and is now owned
Thanks for the nitpick, I've modified the blog entry.
The RISC-V architecture is a potential candidate for
later verification. Would you be interested in trying to keep your C port in the subset of
the C language our verification tools can handle? It may be more work for your project,
but it will give you the real seL4 experience ;-)
If yes, I can give you some tools and instructions on how to use them for checking the
subset. There’s a lightweight syntax-only checker, and there’s a longer-running check that
actually reads the code into the theorem prover.
That will be great. Actually I was thinking of formally verifying the
port, but since I don't have experience with formal verification in
general, I wouldn't know how much time/effort would this take, given
that I heard you did the verification in 20 years and more than 100K
of code :)
On 25.05.2015, at 06:10, Hesham ALMatary
As a warm up, I've written a blog entry  of the project giving some
introductory details for both RISC-V and seL4 microkernel and what has
been done so far. Open to questions/suggestions.
Devel mailing list
The information in this e-mail may be confidential and subject to legal professional
privilege and/or copyright. National ICT Australia Limited accepts no liability for any
damage caused by this email or its attachments.