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" <[email protected]> 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 > [email protected] > https://lists.sourceforge.net/lists/listinfo/genode-main >
------------------------------------------------------------------------------
_______________________________________________ genode-main mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/genode-main
