Re: seL4 Availability (Was: L4.sec)

[htuch]

I'll let Gernot/Gerwin provide a definitive answer here, but just point
out that several (but certainly not all) aspects of the verification work
have already been released under a 3-clause BSD license, including a
bit-vector library, the memory model and separation logic embedding, see:

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

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

Cheers,
Harvey

On Mon, June 11, 2007 01:39, Jonathan S. Shapiro wrote:
> On Sat, 2007-06-09 at 16:38 +1000, Gernot Heiser wrote:
>
>> As to the future status of seL4: We have every intention of providing
>> an open-source implementation of seL4, when it's ready. Whether we'll
>> release a prototype or wait until we have a production version is a
>> management/business decision that will be taken some time in the future.
>>
>>
>> A release of the Haskell prototype is overdue.
>>
>
> What are the release plans for the verification tool chain, if any?
>
>
>
> Jonathan
>
>
>
>
> _______________________________________________
> L4-hurd mailing list
> address@hidden
> http://lists.gnu.org/mailman/listinfo/l4-hurd
>
>