在Dafny之后又扒了一些新的东西 感觉以前FP的页面不太适合塞这些内容了 再开个页面囤一囤东西
Dafny之外
George Necula 97年的博士论文 “Proof-carrying Code” （十年后还评为POPL最佳论文）算是dafny的开始了
(Samit Gulwani 的博导是他 貌似关系巨好 博士论文全是感谢 说什么导师像自己的哥哥一样 带他们划船。。。)
teaching section下的课都可以看看 CS294头几节课和CS263他负责的部分都讲了讲axiomatic semantics 和 Nelson-Oppen method 值得一看
下面几个课也有相关的话题
CS626 Formal Methods @ U Cincinnati
CS389 Automated Logical Reasoning @ UT Austin by Işil Dilig (ş 念 sh) Alex Aiken 的学生
COS516 Automated Reasoning about Software @ Princeton by Aarti Gupta 跟ALR有点像
这本书好像快速的介绍了一下SMT/SAT
南京大学 formal semantics for programming languages 梁红谨
关于Z3(Talk in Compose16)
ETHz的Programming Methodology Group也有很多很好的课 比如Alex Summers 2017 的Program Verification
Why3
一个很好的intro材料是Jean-Christophe Filliâtre的habilitation Matt Fredrikson的课也有很全的作业
Coq
Derek Dreyer和众学生的Semantics课, Aarhus 也用相似的材料。这个课终于让我知道了怎么用vscode写众多verification project里的unicode
Gert Smolka的 ICL
杂
PLDI19学POPL18弄的采访 sigplan对此的宣传
Alex Aiken（我导的导（？）） 最后几段说得挺好的
Z3的负责人 其中一个Nikolaj Bjørner 是 Zohar Manna. Hezinger也是他的学生。
这个夏校有很多相关的内容