It would be very useful to extend sel4's proof techniques to tne genode layer but does not appear feasible given the relatively higher complexity of genode and the c++ runtime.
Hello Ernst,
thank you for the notice. I am very excited about the GPL release of
seL4 and definitely considering it as a base platform for Genode, alone
for the opportunity to get involved with the talented folks at Sydney. I
am happy that the barrier that came with the proprietary development of
seL4 evaporated finally.
Regards
Norman
On 08/04/2014 11:58 PM, Ernst Rohlicek jun. wrote:
> Greetings,
>
> The seL4 microkernel has recently been open-sourced and is now hosted on
> GitHub.
>
> It features high performance and includes proof of formal correctness,
> ie. freedom of bugs.
>
> Maybe this has relevance for your Genode OS framework regarding
> expanding the choice of base platforms.
--
Dr.-Ing. Norman Feske
Genode Labs
http://www.genode-labs.com · http://genode.org
Genode Labs GmbH · Amtsgericht Dresden · HRB 28424 · Sitz Dresden
Geschäftsführer: Dr.-Ing. Norman Feske, Christian Helmuth
------------------------------------------------------------------------------
_______________________________________________
genode-main mailing list
genode-main@...12...ceforge.net
https://lists.sourceforge.net/lists/listinfo/genode-main