Mailing List Archive

On Wed, Sep 24, 2008 at 9:56 AM, Liu Jian <gjk.liu@gmail.com> 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

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

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@gmail.com> wrote:
> On Wed, Sep 24, 2008 at 9:56 AM, Liu Jian <gjk.liu@gmail.com> 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@gmail.org

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