Re: [seL4] FYI: microkernel.info community site
Alexander Senier <[email protected]>
| Newsgroups | gmane.os.genode.devel,gmane.os.hurd.bugs,gmane.os.minix.general,gmane.os.helenos.devel,gmane.comp.micro-kernel.l4.devel,gmane.comp.micro-kernel.l4.sel4.devel |
|---|---|
| Message-ID | <[email protected]> |
Hi Gernot, when analyzing the statement carefully, you'll find that it's indeed true. The seL4 source was *open-sourced* in July 2014 whereas the Muen source was released in August 2013. But of cause you're right, we're not talking about the same properties here. Cheers, Alex On 03/10/2016 10:33 PM, Gernot Heiser wrote: > Interesting statement on the Muen kernel section: "The world’s first Open Source microkernel that has been formally proven to contain no runtime errors at the source code level. “ > > We proved full functional correctness (which is a superset of absence of runtime errors) for seL4 in 2009. I must be missing something. -- Dipl.-Inf. Alexander Senier Scientific Assistant TU Dresden Faculty of Computer Science Institute of System Architecture Chair of Privacy and Data Security 01062 Dresden Tel.: +49 351 463-38719 Fax : +49 351 463-38255 ------------------------------------------------------------------------------ Transform Data into Opportunity. Accelerate data analysis in your applications with Intel Data Analytics Acceleration Library. Click to learn more. http://pubads.g.doubleclick.net/gampad/clk?id=278785111&iu=/4140 _______________________________________________ genode-main mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/genode-main