[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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


  • To: "Liu Jian" <gjk.liu@xxxxxxxxx>
  • From: "Todd Deshane" <deshantm@xxxxxxxxx>
  • Date: Wed, 24 Sep 2008 11:11:23 -0400
  • Cc: xen-research@xxxxxxxxxxxxxxxxxxx
  • Delivery-date: Wed, 24 Sep 2008 08:11:26 -0700
  • Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=message-id:date:from:reply-to:to:subject:cc:in-reply-to :mime-version:content-type:content-transfer-encoding :content-disposition:references; b=FY0dqB5cq/ArCVYxQTCiDWxIah6OiQYu4pWEyGqyqfYn/EwbignGkNcfLSTmzb1RIc eQ6OLVpY8M4zvaOeI1aUG9whqTCqC1EBEoqzvSNRMn5eziLX5rMZpVI75/UX2b+ZcNbO WBG5eKkVoSW80vJW+DYBQVQEDCK6M8YnPCrvA=
  • List-id: Research Issues on Xen <xen-research.lists.xensource.com>

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

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


 


Rackspace

Lists.xenproject.org is hosted with RackSpace, monitoring our
servers 24x7x365 and backed by RackSpace's Fanatical Support®.