关于Dafny的资料
最近在学Dafny，一种可以验证自己的程序语言。本来在rise4fun.com有教学资源，但是现在网站挂了（Waterloo fork了一个网站）在这里囤一下相关的学习材料和笔记。
官方资源
U of Edinburgh 请 KRML 的讲座 介绍了一些历史（尤其是verification的）
Dafny blog 也很不错！
课程资料
UNSW SENG2011 by Albert Nymeyer
UNSW 的 Albert Nymeyer 教授每年开设的 Software Engineering Workshop 2A会完整的覆盖Dafny
16年课程网站 Lecture条目下可以访问课程计划 前四节课的slides可以下载
21年课程网站 很多东西访问不了 但是可以访问他的课件 鸡肋的是访问不了course schedule不知道课件的阅读顺序 但是可以通过文件的修改时间来猜测顺序（我可能会列一下自己看的顺序）
这位同学还善良地留下了自己19年的课程笔记
CMU 15-811 by Bryan Parno
CMU研究生课 Verifying Complex Systems
第一个月会从SAT/SMT开始讲 然后后面三次课学Dafny 两个话题都有相关作业
这门课的内容可能更有用一些。
其他混杂的会提及Dafny的课程（还没有好好看）
Formal software Development Methods @ UIUC 课程网站
Principles of Software @ RPI 课程网站
Systems and Formal Methods (Lecture 3) @ Cornell 课程网站
Formal Methods in Software Engineering @ U of Iowa （请了Leino来讲的） 课程网站
Dafny Mini-course @ ICL 课程网站
以色列某学校 貌似有square root的例子
UNSW SENG2011 笔记
各slides阅读顺序及内容
Hoare Logic
Predicate Translation, Hoare Logic 1 & 2
Intro to Dafny
Dafny Intro, Dafny Basics, Initialisation Strength, Validate Verify
Array Quantifiers, Invariant WYSIWYG, Recursion Termination, Function Predicates, Induction DataTypes
(Examples) Search Insertion Sort, Dutchflag Sort
Sets Sequences
Lemma
Proof Power, Lemma Direct Contra, Lemma Induction Levels, Lemma Induction More, Lemma 100 Prisoners (eg)
Complex Structure
Classes, Verifying Data, Verifying Ghost Data
Examples: Object Dynamic Frames, QuickSort
Some Challenges
第一题有dafny答案
所有题都有dafny solution