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
> [email protected]
> http://lists.gnu.org/mailman/listinfo/l4-hurd
>
>
lmpx.com only provides a reader for public news (NNTP) servers. It is not
affiliated with the servers or forums shown here and is not responsible for
the content of articles, which is written by their respective authors.