TODO:
- 加入两本书:
- https://github.com/gaurangsaini/sipser-computation-3rd-solutions/ 计算理论的
- https://softwarefoundations.cis.upenn.edu/lf-current/Preface.html 程序验证/逻辑/形式语义 相关的（jyy推荐 http://jyywiki.cn/Reading_List， https://blog.jm233333.com/program-verification/ jyy的一个学生 博客可以关注，以及两个相关的课程推荐）
PAPERS:
- Timepiece：用时序逻辑验证网络，在Kirigami基础上引入时序逻辑做模块化验证，包括以往的一系列ryan的做modular verification的文章，都存在一个问题是：需要提前指定正确的数据面状态（数据面计算过程），这样导致用户要做很强/很精确的reasoning（未仿真情况下），否则需要多次验证用户的hypothesis是否可行，极端情况下（即网络真的没有一个收敛解满足requirement） 用户可能需要遍历验证所有数据面的组合结果。
- control plane compressio：未完，压缩细节还没看懂
CODE:
CONFUSIONS:
*
OTHERS:
【之后觉得可行的一个工作】配置压缩：route-map规则，peer group，ip-prefix等等（类似的ACL压缩已经有人做过）。。