我的一些talks:
Understanding IC3, 这是我在研究生一年级上半年末的一个组内分享, 那时的我对verification十分感兴趣, IC3源自SAT-Based Model Checking Without Unrolling. VMCAI'11, 是一个非常有意思的算法. 相关视频可以在video找到.
Proof Assistant Based Verification of Programs, 这是我在研究生一年级下半年的程序分析课上的期末project, 里面旨在使用Agda来形式化数据流算法中经典的"信息流安全分析", 它是我在类型论方向上的第一个尝试, 相关代码你可以在这里找到, 如果你也对类型论十分感兴趣, 那我推荐你看看无穷类型咖啡暑校, 它是我人生中组织的第一个暑校.
PMP: Cost-effective Forced Execution with Probabilistic Memory Pre-planning论文分享, 这是我在上科大第一次做的关于"程序强制执行"的presentation, 也是和我工作相关的一篇文章, 如果你也对强制执行感兴趣, 欢迎打扰我.
The Survey of Symbolic Execution in Software Secuirty, 这是我和GW Yang在研究生一年级上半年的信息安全课上的期末project, 它是关于符号执行的一个小综述.
Detcecting Channel Blocking Errors, 这是我在研究生一年级下半年的程序分析课上的期中论文阅读分享, 它源自Detecting Blocking Errors in Go Programs using Localized Abstract Interpretation. ASE'22. 这篇文章的工作量很足, 如果对自动化检测go中的channel阻塞问题有兴趣可以看看.
Using Modern Linux Security Modules for Enhancing Container Security, 这是我在研究生二年级上半年的高阶分布式系统课上的期末project, 我和GW Yang一起研究了vArmor, 还记得2023的最后一天晚上我们还在实验室讨论vArmor的代码, 成功跨过2023来到了2024. 我其实很看好关于云上的一些安全研究, 这是我的第一次尝试.