Verification

 

在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ørnerZohar Manna. Hezinger也是他的学生。

这个夏校有很多相关的内容