Re: [Xen-research] about formal analysis of Xen

["Liu Jian" <gjk.liu@xxxxxxxxx>]

I am interested in the work about strict formal verification like L4.verfied.
If any information, pls let me know.

Cheers,

Liu Jian

On Wed, Sep 24, 2008 at 11:11 PM, Todd Deshane <deshantm@xxxxxxxxx> wrote:
> On Wed, Sep 24, 2008 at 9:56 AM, Liu Jian <gjk.liu@xxxxxxxxx> wrote:
>> Dear all,
>>
>>   Is there any project or work about the formal analysis of Xen.
>> For example, Using theorem provers, eg. Acl2, isabelle, coq etc.
>> to verify it.  Thanks
>>
>
> The closest thing I can think of is the static analysis that has been
> done or is planned to be done on Xen.
>
> See:
> http://blog.xen.org/index.php/2008/03/04/the-xen-of-static-checking-part-1-bug-free-code-without-the-effort/
> http://lists.xensource.com/archives/html/xen-devel/2008-02/msg00682.html
>
> Cheers,
> Todd
>
>
> --
> Todd Deshane
> http://todddeshane.net
> check out our book: http://runningxen.com
>



-- 
email to: gjk.liu@xxxxxxxxx

_______________________________________________
Xen-research mailing list
Xen-research@xxxxxxxxxxxxxxxxxxx
http://lists.xensource.com/mailman/listinfo/xen-research