The Verification Corner is a video series on YouTube that explains different concepts of software verification.
(opens in new tab)Stepwise refinement – 10/8/2010:
In this episode, Kuat Yessenov and Rustan Leino (opens in new tab), 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 (opens in new tab)
- Channel9 Movie and Podcasts (opens in new tab)
- Chalice Sources [zip] (opens in new tab)
(opens in new tab)Loop Termination – 3/29/2010:
In this episode, Rustan Leino (opens in new tab) 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 (opens in new tab).
- YouTube video (opens in new tab)
- Channel9 Movie and Podcasts (opens in new tab)
- Dafny (opens in new tab) demo project [zip] (opens in new tab)
Specifications in Action – The Chunker – 3/1/2010:
In this episode, Rustan Leino (opens in new tab)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 (opens in new tab)
- Channel9 Movie and Podcasts (opens in new tab)
- Spec# (opens in new tab) Demo project [.zip] (opens in new tab)
Loop Invariants – 1/12/2010:
In this episode, Rustan Leino (opens in new tab)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.
- YouTube video (opens in new tab)
- Channel9 Movie and Podcasts (opens in new tab)
- Whiteboard Slides [pdf] (opens in new tab) [pptx] (opens in new tab)
- Spec# (opens in new tab) Demo project [.zip] (opens in new tab)
-
- Modeling, refinement, and verification (opens in new tab) with Jean-Raymond Abrial
- Using ghost variables and lemmas in a program verification (opens in new tab) with Jason Koenig
- Partial solutions, and comprehensions (opens in new tab) with Rosemary Monahan
- Concurrent programming in Chalice (opens in new tab) with Peter Müller
- 10/8/2010: Stepwise Refinement (opens in new tab) with Kuat Yessenov
- 3/29/2010: Loop Termination (opens in new tab)
- 3/01/2010: The Spec# Chunker (opens in new tab)
- 1/12/2010: Loop Invariants (opens in new tab)
People
Peli de Halleux
Principal Research Software Engineer