EMIC - Software Verification

Download

How do I download the videos?

• To download, right click the file type you would like and pick “Save target as…” or “Save link as…”

Why should I download videos from Channel9?

• It's an easy way to save the videos you like locally.
• You can save the videos in order to watch them offline.
• If all you want is to hear the audio, you can download the MP3!

Which version should I choose?

• If you want to view the video on your PC, Xbox or Media Center, download the High Quality WMV file (this is the highest quality version we have available).
• If you'd like a lower bitrate version, to reduce the download time or cost, then choose the Medium Quality WMV file.
• If you have a Zune, WP7, iPhone, iPad, or iPod device, choose the low or medium MP4 file.
• If you just want to hear the audio of the video, choose the MP3 file.

Right click “Save as…”

• High Quality WMV (PC, Xbox, MCE)
• MP3 (Audio only)
• MP4 (iPod, Zune HD)
• Mid Quality WMV (Lo-band, Mobile)
• WMV (WMV Video)

Today – more than ever – complex software architectures, configurations and the implications of parallel software running on multi-core hardware call for a new methodology to make sure that software is of high-quality and does what it is was designed for. By using a formal approach and going beyond regular software testing the verification team at the  European Microsoft Innovation Center (EMIC), Aachen, Germany are enhancing software verification methods and tools and applying them to analyze 50,000 lines of code in a real life scenario of a market-ready product. This approach is what makes the project unique.

Thomas Santen and Stephan Tobies from EMIC explain what formal software verification is about and how it can help to build reliable systems. The technology they explain is being developed jointly at EMIC and Microsoft’s Research in Software Engineering group (RiSE) in Redmond. Their tool VCC verifies concurrent, low-level C code that is annotated by contracts specifying its intended behavior.

Thomas and Stephan work in the hypervisor verification project Verisoft, which is a collaboration of EMIC, RiSE, along with Wolfgang Paul, professor for computer architecture at the Saarland University in Saarbrücken, Germany. The aim of this project is to verify the hypervisor kernel of Microsoft Hyper-V, Microsoft’s virtualization product. The hypervisor kernel is a small multi-processor operating system micro kernel with memory and thread management but without device drivers. The implementation of this kernel consists of roughly 60 thousand lines of highly optimized C and x64 assembler code.

For further information, please contact Thomas Santen (Thomas.Santen-at-microsoft.com) or Stephan Tobies (Stephan.Tobies-at-microsoft.com).