The Verification Corner - Stepwise Refinement

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)

In this episode of The Verification Corner, Kuat Yessenov and Rustan Leino, Principal Researcher in the Research in Software Engineering (RiSE) group at Microsoft Research,  show how a program can be constructed by stepwise refinement.  First, a high-level description of the program is given.  Then, some more detailed pseudo-code is developed.  Finally, an efficient data-structure representation is chosen and the corresponding changes to the program are written. There are several potential advantages of this approach.  One is that it lets the programmer design the program in finer and finer levels of granularity, rather than having to write all the fine details into the program text at once.  At each level, the verification tool kicks in and checks the correctness, thus proving feedback to the programmer.  A second advantage is that the more abstract descriptions of the program stay around, in a machine readable form that makes sure they stay up-to-date.  This means a new programmer on the project can start reading the more abstract versions in order to understand the program.

• Find past and future episodes of the The Verification Corner!

The Verification Corner is a show on Software Verification Techniques and Tools. The show is produced by the Research in Software Engineering team (RiSE), which coordinates Microsoft's research in Software Engineering in Redmond, USA.