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" <nor...@ge...>
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
> gen...@li...
> https://lists.sourceforge.net/lists/listinfo/genode-main
>
|
