今天最后一天在REUSE了 想囤点东西 这样就可以忘记他们啦！（按照jay的建议）
OS
学到了很多OS知识（真的是为了capture stdout stderr写thread 还有为了telemetry写server才知道我多缺少这方面的东西。。。） 旁听了几节213（还是在PLDI/ISCA某个吃饭活动碰到Brian Railing叫我来听的）
除此之外：
Sergio Benitez 的 OS课给每个人都送了一个raspberry pi 4 然后直接在上面写OS
MIT的xv6，居然当时是russ cox跟导师一起写的。。。 书很短很精炼
JYY的OS课 他在知乎上还吹了SJTU的银杏书 那个组发表量页太恐怖了。。。 Haibo Chen OSDI 2023 6篇。。。
JYY今年Usenix ATC还发了个OS education的paper 有点想看一看（名字也很搞）
感觉南大和SJTU那个组也值得看一看
PL/Verification
终于读了Z3和eggraphs的tutorial。最大的惊讶是在读Bradley&Manna的课本的时候发现Real Arithmetic是decidable的，也是很神奇。
Verus
Bryan 人真的太好了 真的是神人，， 这个组真的是梦中情组。虽然REUSE老美真的很多，也没有在匹兹堡找到什么生活乐趣（我也不懂 感觉既没找到work life balance 工作上又没有太大的成就感），但是能end up here真的很好！
工作上最大的收获可能是对programming with triggers更熟悉了，也稍微了解了一下SMT encoding到底是怎么做成的。
Verus的话想继续跟进下去 有可能找些good first issue帮帮忙吧！Prusti（Viper）也想试一试，RustHornBelt和各种Rust foundations也想看一看（希望我现在有这个基础了）。这里就码一下相关的事儿吧：
Prusti相关的
他们很多本科生/硕士生跟着这个project就会把thesis写成prusti相关的
Christoph Matheja的简介slides 他们肯定开课让穷苦学生写prusti了
他们网站上还有一串巨大的介绍
MPI相关的
主要就是Ralf Jung和Derek Dreyer写的RustBelt相关的paper，后面还上了CACM。youtube上也有很多视频可以先看看
最近的Rust verification的technical paper
还有一个Leveraging Rust Types for synthesis的，看着也很有意思。
System Verification相关的
主要是UW Xi Wang和Emina Torlak那个组的工作，可能最有名的就是Push Button
不过我system都不知道一点 可能看这个太快了 也许看看银杏书的advanced chapters再说吧
其实Bryan组里之前的工作我也不是很了解，也许什么时候知道更多systems相关的事儿的时候再回来看看吧
WhyML
对于intermediate verification language而言，感觉现在只有WhyML在不是Z3的solver有很好的结果
Matt Fredrikson的Bug Catching课从16年的dafny换成了现在的WhyML，也许是在美国入门的好课
Ivy和decidable Logic
主要是看Oded Padon以前的工作 能有finite model for counterexample貌似是一个很好的性质