Download this episode
In this episode of The Verification Corner, Rustan Leino talks about Loop Invariants. He gives a brief summary of the theoretical foundations and shows how a program can sometimes be systematically constructed from its specifications. Rustan Leino is a Principal Researcher in the Research in Software Engineering (RiSE) group at Microsoft Research.
- Try Spec# in your web browser at http://rise4fun.com/specsharp!
- Whiteboard slides [.pdf] [.pptx]
- Spec# Demo project [.zip]
- 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) coordinates Microsoft's research in Software Engineering in Redmond, USA.
Available formats for this video:
Actual format may change based on video formats available and browser capability.