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.
Comments have been closed since this content was published more than 30 days ago, but if you'd like to send us feedback you can Contact Us.