>>>>> On Mon, 11 Jun 2007 10:28:37 +1000 (EST), [EMAIL PROTECTED] 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. Gernot _______________________________________________ L4-hurd mailing list [email protected] http://lists.gnu.org/mailman/listinfo/l4-hurd
