Automatic Program Verification: Isar and Dafny Methods
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
lemma
name: P
proof
hence
Q
by
sledgehammer
hence
R
by
simp
thus
S
by
grind
end
lemma
name: P
proof
assert
Q
by
sledgehammer
assert
R
by
simp
assert
S
by
grind
end
ghost method
name()
ensures
P
{assert
Q
by
sledgehammer
assert
R
by
simp
assert
S
by
grind
}
ghost method
name()
ensures
P
{assert
Q
by
dafny
assert
R
by
dafny
assert
S
by
dafny
}
ghost method
name()
ensures
P;
{assert
Q;
assert
R;
assert
S;
}
Ghost variables, ghost code
FindZero continued
Object structures
List
•
List
•
http://rise4fun.com/Dafny/MbH
•
RockBand
•
http://rise4fun.com/Dafny/wjD
•
Dafny
•
research.microsoft.com/dafny
•
rise4fun
•
rise4fun.com
•
Verification Corner
•
research.microsoft.com/verificationcorner
© 2007 Microsoft Corporation. All rights reserved. Microsoft, Windows, Windows Vista and other product names are or may be registered trademarks and/or trademarks in the U.S. and/or other countries.
The information herein is for informational purposes only and represents the current view of Microsoft Corporation as of the date of this presentation. Because Microsoft must respond to changing market conditions, it should not be interpreted to be a commitment on the part of Microsoft, and Microsoft cannot guarantee the accuracy of any information provided after the date of this presentation.
MICROSOFT MAKES NO WARRANTIES, EXPRESS, IMPLIED OR STATUTORY, AS TO THE INFORMATION IN THIS PRESENTATION.
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. 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.
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
