Automatic Program Verification: Isar and Dafny Methods

Explore the concepts of automatic program verification using Isar and Dafny methods, including lemmas, ghost variables, code structures, and exercises. Dive into the research and tools available for program verification in software engineering.

• Program Verification
• Isar
• Dafny
• Software Engineering
• Research

ail_co Follow

Uploaded on Sep 14, 2024 | 0 Views

Download Presentation

Please find below an Image/Link to download the presentation.

The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.

Presentation Transcript

1. Using and Building an Automatic Program Verifier K. Rustan M. Leino Research in Software Engineering (RiSE) Microsoft Research, Redmond Lecture 2 Marktoberdorf Summer School 2011 Bayrischzell, BY, Germany 6 August 2011

2. Isar and Dafny lemma name: P proof hence Q by sledgehammer hence R by simp thus S by grind end

3. Isar and Dafny lemma name: P proof assert Q by sledgehammer assert R by simp assert S by grind end

4. Isar and Dafny ghost method name() ensures P { assert Q by sledgehammer assert R by simp assert S by grind }

5. Isar and Dafny ghost method name() ensures P { assert Q by dafny assert R by dafny assert S by dafny }

6. Isar and Dafny ghost method name() ensures P; { assert Q; assert R; assert S; }

7. Ghost variables, ghost code FindZero continued

8. Object structures List

9. Exercises List http://rise4fun.com/Dafny/MbH RockBand http://rise4fun.com/Dafny/wjD

10. Links Dafny research.microsoft.com/dafny rise4fun rise4fun.com Verification Corner research.microsoft.com/verificationcorner