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 by GD.
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. Cheers, Gerwin > On 25.05.2015, at 06:10, Hesham ALMatary <heshamelmat...@gmail.com> wrote: > > Hi all, > > As a warm up, I've written a blog entry [1] 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. > > > [1] > http://heshamelmatary.blogspot.co.uk/2015/05/porting-sel4-to-risc-v-status-report-no1.html > > Thanks, > -- > Hesham > > _______________________________________________ > Devel mailing list > Devel@sel4.systems > https://sel4.systems/lists/listinfo/devel ________________________________ 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. _______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
