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.
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.If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.
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.
E N D
Presentation Transcript
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
Isar and Dafny lemma name: P proof hence Q by sledgehammer hence R by simp thus S by grind end
Isar and Dafny lemma name: P proof assert Q by sledgehammer assert R by simp assert S by grind end
Isar and Dafny ghost method name() ensures P { assert Q by sledgehammer assert R by simp assert S by grind }
Isar and Dafny ghost method name() ensures P { assert Q by dafny assert R by dafny assert S by dafny }
Isar and Dafny ghost method name() ensures P; { assert Q; assert R; assert S; }
Ghost variables, ghost code FindZero continued
Object structures List
Exercises List http://rise4fun.com/Dafny/MbH RockBand http://rise4fun.com/Dafny/wjD
Links Dafny research.microsoft.com/dafny rise4fun rise4fun.com Verification Corner research.microsoft.com/verificationcorner
