北京时间2022年4月1日晚，华为德累斯顿研究所所长付明老师给课题组师生做了题为“Practical Formal Verification: Smart and Safe Concurrency for Modern Hardware”的在线报告。在报告中，付明老师介绍了硬件发展对并发程序的挑战，分享了团队的相关工作，包括辅助优化和验证弱内存模型架构下同步原语的VSync框架、针对多层NUMA系统的可组合的锁框架CLoF、以及相关技术在大规模代码中的性能优化和漏洞发现。同时，付明老师结合在高校和企业科研工作的不同感受，和课题组师生进行了分享交流。报告丰富深入的技术内容和轻松开放的交流讨论给了大家很多指导与启发。
报告人简介：付明博士，2017年加入华为，现任华为操作系统和形式化方法技术专家，华为德累斯顿研究所所长。主要研究方向包括程序语言理论、并发理论、并发程序验证和操作系统形式化验证，曾在操作系统和形式化方法知名学术会议SOSP、ASPLOS、POPL和CAV上发表多篇论文，并获得ASPLOS'21杰出论文奖。加入华为前任职于中国科学技术大学计算机学院，主要学术成果包括基于并发精化验证理论在定理证明工具Coq中构建了支持抢占的操作系统内核验证平台，完成商用实时嵌入式系统uC/OS-II核心功能模块的形式化验证。