球友会qy

天基综合信息系统全国重点实验室2025年度鲁班论坛第8期

报告主题一：Derivative-Agnostic Inference of Nonlinear Hybrid Systems

时 间：2025年6月10日 （周二） 14:00-15:00

地 点：中国科研实验室软件研究所5号楼4层第一会议室

主讲人：陈明帅，浙江大学，百人计划研究员

报告摘要：

This talk addresses the problem of inferring a hybrid automaton from a set of input-output traces of a hybrid system exhibiting discrete mode switching between continuously evolving dynamics. Existing approaches mainly adopt a derivative-based method where (i) the occurrence of mode switching is determined by a drastic variation in derivatives and (ii) the clustering of trace segments relies on signal similarity -- both subject to user-supplied thresholds. In this talk, I present a derivative-agnostic approach, named Dainarx, to infer nonlinear hybrid systems where the dynamics are captured by nonlinear autoregressive exogenous (NARX) models. Dainarx employs NARX models as a unified, threshold-free representation through the detection of mode switching and trace-segment clustering. We show that Dainarx suffices to learn models that closely approximate a general class of hybrid systems featuring high-order nonlinear dynamics with exogenous inputs, nonlinear guard conditions, and linear resets. Experimental results on a collection of benchmarks indicate that our approach can effectively and efficiently infer nontrivial hybrid automata with high-order dynamics yielding significantly more accurate approximations than state-of-the-art techniques.

报告人介绍：

陈明帅，浙江大学研究员、博士生导师、启真学者，CCF形式化方法专委执行委员，国家优秀青年基金（海外）取得者。2019年于中国科研实验室软件研究所获计算机软件与理论专业博士学位，此后于德国RWTH Aachen从事为期3年的博士后研究工作，2023年初加入浙江大学。主要研究方向包括形式验证、程序理论、概率/量子系统、信息物理融合系统、AI4FM等，与合作者一起，提出新型安全攸关系统形式验证理论，解决了概率程序不动点估计、微分系统可达性判定、时滞系统高效控制生成等若干软件理论难题，研究成果应用于我国探月二期工程“嫦娥”三号等重大工程，在Inf. Comput.、IEEE Trans. Automat. Contr.、OOPSLA、CAV、FM、ASPLOS、ASE等领域旗舰期刊/会议上发表学术论文40余篇，曾获中科院院长特别奖、ATVA杰出论文奖、FMAC最佳论文奖。

报告主题二：AI³: Abstract Interpretation, Automated Inference, Artificial Intelligence?

时 间：2025年6月10日 （周二） 15:00-16:00

地 点：中国科研实验室软件研究所5号楼4层第一会议室

主讲人：王钟逸，浙江大学，博士生（导师：陈明帅）

报告摘要：

基于抽象解释的可靠静态分析技术可以扫描程序中的潜在缺陷，并在风险代码处插入待检测断言（报警），但往往受限于精度损失而产生大量误报，因此需要专家手动精化分析策略或核查断言。基于演绎推理的自动定理证明技术可以验证断言是否为真，但依赖于专家人工构建的形式规约。本报告将介绍待检测断言制导的定理证明与抽象解释融合验证框架。报告的第一部分介绍静态分析抽象策略自适应精化方法，该方法将多种抽象策略对应的外部参数建模为具有完全格结构的参数空间上的随机变量，并引入在线学习思想，基于Sample-Analyze-Refine迭代实现首个渐增式全自动静态分析参数精调方法。实验结果表明该方法能够有效平衡静态分析准确率与效率，特别是在大规模真实程序上具有明显优势。报告的第二部分介绍大语言模型驱动的程序规约生成方法，该方法针对待检测断言顺利获得静态分析技术划分代码功能模块，利用每个模块的程序上下文、验证义务等信息构造提示词，指导大模型生成必要的功能性规约。初步实验结果表明该方法能够有效验证程序内存安全性及挖掘潜在运行时错误。

报告人介绍：

王钟逸，浙江大学计算机科学与技术学院博士生，导师是陈明帅研究员。主要研究方向是程序静态分析与自动化验证。相关研究成果发表于ASE、J.Comput.Sci.Technol.等领域重要国际会议/期刊。