 Home |
Products |
Support |
Community |
News |
xen-research
Re: [Xen-research] about formal analysis of Xen
| To: | deshantm@xxxxxxxxx, xen-research@xxxxxxxxxxxxxxxxxxx |
|---|---|
| Subject: | Re: [Xen-research] about formal analysis of Xen |
| From: | "Liu Jian" <gjk.liu@xxxxxxxxx> |
| Date: | Thu, 25 Sep 2008 11:03:47 +0800 |
| Cc: | |
| Delivery-date: | Thu, 25 Sep 2008 05:55:39 -0700 |
| Dkim-signature: | v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=domainkey-signature:received:received:message-id:date:from:to :subject:in-reply-to:mime-version:content-type :content-transfer-encoding:content-disposition:references; bh=nNyQVVdSMlvPR/rh/tunLR2IlxYoVPIv/NJcrvjF+9s=; b=hDELO8dP1tmfzqDgPjs/iiB79ctGoqXcVGTKlVzHAfSPHSKiJZte0lIwD91hkC4thj sUTZNo0TOPPHpBT/KYLF4RUCeVQigPDjoeTFkEDlC7o8kWNE1IWocCEOODPd0w5G2mMe U8a6ThhSFhEe0kkXUeZ2LEm84fIbLBIra9T0Q= |
| Domainkey-signature: | a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=message-id:date:from:to:subject:in-reply-to:mime-version :content-type:content-transfer-encoding:content-disposition :references; b=I5AUZiCYk/kVvJ0+r+TMtOwgFuIXJBRoOxcEcLx4XwnfVSopBxtTUyAvvaVz5Ty3ot nZse6CiiyaPQpEefeITmt8+zDuHSOWRXfExy6q4oI4QuS/Z1TFgL5UA7lpt+/UOwHcqO nyHDuC1uITKGLLn+Ske3OwTQCrRRfhlqusf+0= |
| Envelope-to: | www-data@xxxxxxxxxxxxxxxxxxx |
| In-reply-to: | <1e16a9ed0809240811x3ec10a3cg2e075ff0ca52b363@xxxxxxxxxxxxxx> |
| List-help: | <mailto:xen-research-request@lists.xensource.com?subject=help> |
| List-id: | Research Issues on Xen <xen-research.lists.xensource.com> |
| List-post: | <mailto:xen-research@lists.xensource.com> |
| List-subscribe: | <http://lists.xensource.com/mailman/listinfo/xen-research>, <mailto:xen-research-request@lists.xensource.com?subject=subscribe> |
| List-unsubscribe: | <http://lists.xensource.com/mailman/listinfo/xen-research>, <mailto:xen-research-request@lists.xensource.com?subject=unsubscribe> |
| References: | <8c2dc7030809240656m7cb5689cn2a00852285d257a5@xxxxxxxxxxxxxx> <1e16a9ed0809240811x3ec10a3cg2e075ff0ca52b363@xxxxxxxxxxxxxx> |
| Sender: | xen-research-bounces@xxxxxxxxxxxxxxxxxxx |
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 |
| <Prev in Thread] | Current Thread | [Next in Thread> |
|---|---|---|
| ||
| Previous by Date: | [Xen-research] Motivation?, Y. DU |
|---|---|
| Next by Date: | [Xen-research] Re: Motivation?, Andres Lagar-Cavilla |
| Previous by Thread: | Re: [Xen-research] about formal analysis of Xen, Todd Deshane |
| Next by Thread: | [Xen-research] what is "native execution" of apps?, 刘志建 |
| Indexes: | [Date] [Thread] [Top] [All Lists] |
