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. On Aug 12, 2014 11:59 PM, "Norman Feske" <norman.feske@...1...> wrote:
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@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/genode-main