2026年6月6日，91看片 举办“两校名师讲堂”，特邀北京大学计算机学院詹乃军教授，作了题为“国产多核实时操作系统微内核形式验证”的学术讲座，院长童向荣、学院科研骨干教师及部分研究生代表参加。

讲座中，詹乃军教授介绍了近年完成的一个某国产多核实时操作系统微内核形式验证工作。验证的核心模块包括：任务管理与调度、中断和异常处理、任务同步与通信、核间通信与动态重构、时钟管理、权能访问控制、分区配置和分区通信，总计2万5千行代码。最后，简要介绍了最近提出的关于操作系统等基础软件验证新框架，可以大幅提高验证效率和自动化水平，降低验证人力成本。

报告现场气氛热烈，互动环节师生踊跃提问。本次报告为烟大91看片 师生带来了形式化方法前沿发展的深刻洞察，极大地激发了大家的求知热情与创新思考。

专家简介：

詹乃军，北京大学计算机学院博雅特聘教授，国家杰出青年科学基金获得者。之前，为中科院软件所研究员，中科院特聘研究员，中国科学院大学岗位教授，计算机科学国家重点实验室执行主任。分别在南京大学数学系（1989-1993）和南京大学计算机系（1993-1996）获得学士和硕士学位，在中国科学院软件研究所获得博士学位（1997-2000）。研究方向包括：形式化方法，实时、嵌入式、混成系统，程序验证等。任《Journal of Automated Reasoning》、《Formal Aspects of Computing》、《J. of Logical and Algebraic Methods in Programming》、《Research Direction: Cyber-Physical Systems》、《软件学报》、《计算机研究与发展》《电子学报》、《前瞻科技》等期刊编委，国际会议MEMOCODE和SETTA的指导委员会委员，多个国际会议程序委员会共同主席（如形式化方法旗舰会议FM 2021 和验证领域顶级会议TACAS 2027）和著名国际会议程序委员会委员（如CAV、RTSS、HSCC、ICCPS、EMSOFT等）；在著名国际会议和杂志发表论文150多篇，出版专著2部，编著4部，国际国内著名杂志专刊9辑等。现任CCF形式化方法专委主任。

作者：郑强   责任编辑：马文明   审核：段昕