http://mschnlnine.vo.llnwd.net/d1/Dev/App_Themes/C9/images/feedimage.pnghttp://channel9.msdn.com/tags/C/chttp://channel9.msdn.com/tags/C/en-usWed, 28 Jan 2009 21:09:31 GMTWed, 28 Jan 2009 21:09:31 GMTEvNet (EvNet, Version=1.0.3608.3122, Culture=neutral, PublicKeyToken=null)<img src="http://mschnlnine.vo.llnwd.net/d1/ch9/8/6/4/5/5/4/koskalverifiedc_small_ch9.jpg" border="0" />Michal Moskal gives us a short introduction at the <a href="http://research.microsoft.com/vcc/">Verifying C Compiler</a> (VCC) project. VCC is a tool that proves correctness of annotated concurrent C programs or finds problems in them. VCC extends C with design by contract features, like pre- and postcondition as well as type invariants. The current primary goal of the VCC project is to to verify <a href="http://www.microsoft.com/servers/hyper-v-server/default.mspx">Microsoft Hyper-V</a>. Hyper-V is a hypervisor -- a thin layer of software that sits just above the hardware and beneath one or more operating systems. The Hypervisor verification project is a cooperation between <a href="http://www.microsoft.com/emic/default.mspx">European Microsoft Innovation Center</a> in Aachen, Germany the <a href="http://research.microsoft.com/rise">RiSE</a> group at <a href="http://research.microsoft.com/">Microsoft Research</a> in Redmond and the <a href="http://www.uni-saarland.de/en/">Saarland University</a> in Saarbrücken, Germany.<br /> <br /> <ul> <li><a href="http://research.microsoft.com/en-us/projects/vcc/vcc-msrc-2008-full.pdf">VCC slide deck</a>, get the high-level picture and more details, </li> <li><a href="http://research.microsoft.com/vcc">VCC home page</a>, all you want to know. </li> <li>Unfortunately, there is currently no download available of VCC.  </li> </ul> <br /> <p><em>The </em><a href="http://research.microsoft.com/rise"><em>Research in Software Engineering team</em></a><em> (RiSE) coordinates Microsoft's research in Software Engineering in Redmond, USA.</em> </p><img src="http://channel9.msdn.com/455468/WebViewBug.aspx?EVT=0" height="1" width="1" alt="" />http://channel9.msdn.com/posts/Peli/Michal-Moskal-and-The-Verified-C-Compiler/http://channel9.msdn.com/posts/Peli/Michal-Moskal-and-The-Verified-C-Compiler/Fri, 30 Jan 2009 10:25:00 GMThttp://mschnlnine.vo.llnwd.net/d1/ch9/8/6/4/5/5/4/koskalverifiedc_ch9.wmv49878http://channel9.msdn.com/455468/WebViewBug.aspx?EVT=0Michal Moskal gives us a short introduction at the Verifying C Compiler (VCC) project. VCC is a tool that proves correctness of annotated concurrent C programs or finds problems in them. VCC extends C with design by contract features, like pre- and postcondition as well as type invariants.Peli de Halleux0http://channel9.msdn.com/posts/Peli/Michal-Moskal-and-The-Verified-C-Compiler/RSS/http://channel9.msdn.com/455468/Trackback.aspxCCompilersHyperVresearchriseSoftware Engineering ResearchTestingvccverification