<p>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.</p>
<div class="gmail_quote">On Aug 12, 2014 11:59 PM, "Norman Feske" <<a href="mailto:norman.feske@...1...">norman.feske@...1...</a>> wrote:<br type="attribution"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Hello Ernst,<br>
<br>
thank you for the notice. I am very excited about the GPL release of<br>
seL4 and definitely considering it as a base platform for Genode, alone<br>
for the opportunity to get involved with the talented folks at Sydney. I<br>
am happy that the barrier that came with the proprietary development of<br>
seL4 evaporated finally.<br>
<br>
Regards<br>
Norman<br>
<br>
On 08/04/2014 11:58 PM, Ernst Rohlicek jun. wrote:<br>
> Greetings,<br>
><br>
> The seL4 microkernel has recently been open-sourced and is now hosted on<br>
> GitHub.<br>
><br>
> It features high performance and includes proof of formal correctness,<br>
> ie. freedom of bugs.<br>
><br>
> Maybe this has relevance for your Genode OS framework regarding<br>
> expanding the choice of base platforms.<br>
<br>
--<br>
Dr.-Ing. Norman Feske<br>
Genode Labs<br>
<br>
<a href="http://www.genode-labs.com" target="_blank">http://www.genode-labs.com</a> · <a href="http://genode.org" target="_blank">http://genode.org</a><br>
<br>
Genode Labs GmbH · Amtsgericht Dresden · HRB 28424 · Sitz Dresden<br>
Geschäftsführer: Dr.-Ing. Norman Feske, Christian Helmuth<br>
<br>
------------------------------------------------------------------------------<br>
_______________________________________________<br>
genode-main mailing list<br>
<a href="mailto:genode-main@lists.sourceforge.net">genode-main@...12...ceforge.net</a><br>
<a href="https://lists.sourceforge.net/lists/listinfo/genode-main" target="_blank">https://lists.sourceforge.net/lists/listinfo/genode-main</a><br>
</blockquote></div>