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.