我的一些talks:
Understanding IC3, 这是我在研究生一年级上半年末的一个组内分享, 那时的我对verification十分感兴趣, IC3源自SAT-Based Model Checking Without Unrolling. VMCAI'11, 是一个非常有意思的算法.
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阻塞问题有兴趣可以看看.