[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: seL4 Availability

From: Gernot Heiser
Subject: Re: seL4 Availability
Date: Mon, 11 Jun 2007 12:15:26 +1000 (EST)

>>>>> On Mon, 11 Jun 2007 10:28:37 +1000 (EST), address@hidden said:
h> I'll let Gernot/Gerwin provide a definitive answer here, but just point
h> out that several (but certainly not all) aspects of the verification work
h> have already been released under a 3-clause BSD license, including a
h> bit-vector library, the memory model and separation logic embedding, see:

h> http://ertos.nicta.com.au/research/l4.verified/kmalloc.pml

h> A future release is planned of the the later with improved support for C's
h> structure types in the near future.

Just to clarify: While I said that we intend to keep the kernel open
source, that doesn't mean we're committed to open-source the complete
verification. This is, again, a business decision which is heavily
dependent on factors that are simply not known at this time.


reply via email to

[Prev in Thread] Current Thread [Next in Thread]