11 Mar
2016
11 Mar
'16
3:03 p.m.
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