The Verification Corner is a video series on YouTube that explains different concepts of software verification.
Stepwise refinement – 10/8/2010:
In this episode, 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.
- YouTube video
- Channel9 Movie and Podcasts
- Chalice Sources [zip]
Loop Termination – 3/29/2010:
In this episode, Rustan Leino shows how to prove loop termination. During his demonstration, Rustan presents the theoretical background information necessary to build the proof before modeling it using the Dafny language.
- YouTube video
- Channel9 Movie and Podcasts
- Dafny demo project [zip]
Specifications in Action – The Chunker – 3/1/2010:
In this episode, Rustan Leino writes a string chunker using Spec#. He gives a brief overview how one can specify and implement a program while getting the help from the Spec# verifier.
- YouTube video
- Channel9 Movie and Podcasts
- Spec# Demo project [.zip]
Loop Invariants – 1/12/2010:
In this episode, Rustan Leino talks about Loop Invariants. He gives a brief summary of the theoretical foundations and shows (using a problem to compute cubes) how a program can sometimes be systematically constructed from its specifications.
-
- Modeling, refinement, and verification with Jean-Raymond Abrial
- Using ghost variables and lemmas in a program verification with Jason Koenig
- Partial solutions, and comprehensions with Rosemary Monahan
- Concurrent programming in Chalice with Peter Müller
- 10/8/2010: Stepwise Refinement with Kuat Yessenov
- 3/29/2010: Loop Termination
- 3/01/2010: The Spec# Chunker
- 1/12/2010: Loop Invariants
People
People
Peli de Halleux
Principal RSDE