OSDI20——Fast-RDMA-based-Ordered-Key-Value-Store-using-Remote-Learned-Cache Step 1 题目摘要引言 Title Fast RDMA-based Ordered Key-Value Store usng Remote Learned Related work: RDMA-based ordered Key-Value store like DrTM-Tree,Cell, eRPC+Masstree Abstract RDMA has gained con 2020-12-14 Research Paper 三步法 Paper
Coq学习——《Software-Foundation》Volume1.9-ProofObjects ProofObjects: The Curry-Howard Correspondence "Algorithms are the computational content of proofs." --Robert Harper In Coq we have seen machanisms for Programming: using inductive d 2020-12-10 Computer Science 形式化验证 形式化验证
Coq学习——《Software-Foundation》Volume1.8-Maps Maps Definition total maps and partial maps. A nice case study using ideas we've seen in previous chapters, including building data structures out of high-order functions and the use of reflection t 2020-12-10 Computer Science 形式化验证 形式化验证
专业之外，社区之中 专业之外，社区之中 晚上回家前买到了心心念念 Fascino 面包，和师弟讨论了一个半钟的 RG 选题与我眼中的计算机科学，总算空闲下来，可以整理一下 13 周的碎碎念了。 本周做了不少有意思的事情，除了继续定理证明器的学习，还开始联络校外毕设申请与题目选定，周六则和老徐在班级群里隔空“对线”，今天又出门参加的流浪犬救助领养活动与长宁区新华社区原创作品设计大赛成果展。 倒叙说说吧，下午非常幸 2020-12-06 Life 随笔 随笔
Z3学习——Z3-guide Introduction What is Z3 Z3 is a state-of-art theorem prover from Microsoft Research. Check sat of logical formulas. Match for software analysis and verification tools. Low level tool. Basic Comma 2020-12-03 Computer Science 形式化验证 形式化验证