时间：2026年5月11日（周一）上午9:00-11:40
地点：岳麓山校区计算机楼313
报告一（9:00-9:40）
报告人：许进教授，北京大学
题目：从生物计算到探针计算机
报告摘要：电子计算机难以有效求解所谓的“组合爆炸”问题。这类问题的显著特点是随着问题规模的增加，所需的计算量会呈指数级增长。它们属于NP完全问题，例如资源分配、逻辑电路设计、路径规划、蛋白质结构预测、密码破译等等。由于所有NP完全问题本质上是等价的，我们只需深入研究其中一类NP完全问题，便能将所得结论推广至其他所有NP完全问题。围绕图着色这一典型的NP完全问题，报告人将从图的结构与构造、相关算法设计，到对计算模型的探索展开汇报。在计算模型方面，介绍了并行型DNA计算模型，基于该模型，项目组完成了61个顶点图着色问题的求解实验，使生物计算的搜索规模达到了359，为迄今国际上最大规模的生物实验。受DNA计算模型及其硬件实现的启发，报告人提出了一种底层并行计算的9-元组计算模型，称为探针机。其数据是多维的，“探针”是类比生物技术中的概念，用于寻找特定数据，并把它们关联起来的“粘合剂”，探针算子独立并行运算。介绍了基于生物和电子技术的两类探针计算机模型。其中，阻断非解生物型探针计算系统成功应用于求解114个顶点的图着色问题，展现了生物计算在复杂问题求解中的潜力。基于FPGA卡的电子探针计算机具有高并行性、可扩展性以及对NP完全问题的通用求解能力，为高效计算提供新思路。
报告人简介：许进，北京大学教授， 北京工商大学计算机与人工智能24小时娱乐线路检测院长，博士生导师。理学、工学双博士。长期从事理论计算机、生物计算、图论与组合优化等研究。出版学术独著6部，发表学术论文300余篇。作为第一完成人，获国家自然科学二等奖1项、教育部自然科学一等奖2项、湖北省自然科学一等奖1项。先后主持国家自然科学基金重点项目、重大国际合作项目、专项基金项目、重大仪器专项、863项目、国家重大工程、国家重点研发计划共超十项。现任中国电子学会电路与系统分会副主任委员、中国通信学会云计算与大数据委员会副主任委员、中国网络空间安全协会理事、中国电子学会电路与系统分会生物计算与生物信息处理专委会理事长、《广州大学学报（自然科学版）》主编，《Artificial Intelligence Review》与《电子与信息学报》副主编，《电子学报》、《计算机学报》、《软件学报》等编委；曾任军委科学技术委领域专家、中国电子学会电路与系统分会图论与系统优化专委会理事长、湖北省运筹学会理事长、北京市运筹学会副理事长、教育部网络空间安全教咨委委员；第一、二、四、五、七、八届国际生物计算机大会主席；2021年中国科24小时娱乐线路检测院士初步候选人，2022年应邀作中国科24小时娱乐线路检测信息学部学术年会大会报告。
报告二（9:40-10:20）
报告人：潘纲教授，浙江大学
题目：脑机解码与大模型
报告摘要：人工智能、计算神经科学、微电子、神经生理学等领域的最新进展，显示出计算机和生命体之间的融合成为可能并日趋明显。以脑机接口为代表的神经技术的突破使得脑与计算机之间的结合越来越紧密，脑机融合及其一体化已成为人工智能发展的一个重要趋势,如何对神经信息的解读与利用是一个重要课题。本报告将在介绍新型智能形态――脑机智能的基础上，重要分享课题组在神经信号解码、脑电大模型、脑机赋能大模型等方面的研究进展与实践。
报告人简介：浙江大学计算机24小时娱乐线路检测求是特聘教授，脑机智能全国重点实验室主任，国家杰出青年科学基金获得者，中国认知科学学会副理事长，中国人工智能学会会士、脑机融合与生物机器智能专委会主任委员，中国自动化学会机器人智能专委会副主任委员等。研究方向为类脑计算、脑机接口、人工智能等。指导学生获多项国际会议或期刊的最佳论文奖、最佳论文提名奖、时间考验论文奖。
报告三（10:20-11:00）
报告人：詹乃军教授，北京大学
题目：国产多核实时操作系统微内核形式验证
报告摘要：本报告简要介绍我们项目组近年完成的一个某国产多核实时操作系统微内核形式验证工作。验证的核心模块包括：任务管理与调度、中断和异常处理、任务同步与通信、核间通信与动态重构、时钟管理、权能访问控制、分区配置和分区通信，总计2万5千行代码。为此，我们发展了基于CSL-R的操作系统功能性验证框架以及基于信息流分析的信息安全性验证框架，首次提出了针对DSP的WCET分析技术并实现工具。总计 实现Coq验证代码45万行左右，发现并纠正了20多类数百个错误，为该款在某重点领域应用操作系统顺利通过CC EAL5+认证。最后，简要介绍我们最近提出的关于操作系统等基础软件验证新框架，可以大幅提高验证效率和自动化水平，降低验证人力成本。
报告人简介：詹乃军，男，1971年5月生，北京大学计算机24小时娱乐线路检测博雅特聘教授，国家杰出青年科学基金获得者。之前，为中科院软件所研究员，中科院特聘研究员，中国科24小时娱乐线路检测大学岗位教授，计算机科学国家重点实验室执行主任。分别在南京大学数学系（1989-1993）和南京大学计算机系（1993-1996）获得学士和硕士学位，在中国科24小时娱乐线路检测软件研究所获得博士学位（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形式化方法专委主任。
报告四（11:00-11:40）
报告人：尹一通教授，南京大学
题目：马尔可夫链的并行化
报告摘要：以单点动态系统（single-site dynamics）为代表的马尔可夫链，是求解高维采样问题的经典算法框架，在统计推断、高维积分、复杂系统模拟等关键应用中发挥着基础性作用。此类马尔可夫过程具有固有的串行特性——长期以来，针对此类串行过程，如何实现高效并行化始终是悬而未决的关键挑战；而对于复杂系统的模拟、推断与学习，此类计算任务是否具有“本质串行性”，更是关乎人工智能领域并行计算发展前景的关键科学问题。在本报告中，我将介绍我们近期提出的马尔可夫过程并行化新方法：在满足相关性衰减的渐进 Dobrushin 条件下，构建了适用于单点动态系统马尔可夫链的通用高效并行化算法。这一发现从理论上改变了长久以来人们对于马尔可夫过程难以并行化的认识。
报告人简介：尹一通，南京大学计算机24小时娱乐线路检测教授，研究领域为理论计算机科学，主要研究兴趣包括随机算法、计算采样理论、数据结构、并行与分布式计算理论等，在JACM、SICOMP、STOC、FOCS、SODA等理论计算机科学重要期刊与会议发表论文数十篇。入选新基石研究员，主持国家重点研发计划和自然科学基金优青等项目，获IEEE-CS青年科学家等荣誉，指导博士生获CCF优博以及入选CCF博士学位论文激励计划。目前担任南京大学理论计算机科学团队负责人。
