7月6日下午，由中国计算机学会（CCF）主办、CCF形式化方法专业委员会和江西师范大学人工智能学院(原计算机信息工程学院)联合承办的“CCF走进高校”活动在江西师范大学先骕楼4218会议室举行。

活动邀请中国科学院软件研究所宋富研究员、南京大学计算机学院时清凯副教授、同济大学计算机科学与技术学院刘关俊教授、北京大学数学科学学院孙猛教授、浙江大学区块链与数据安全全国重点实验室袁胜浩研究员、中国科学院软件研究所吴志林研究员做主题报告。校党委副书记汪洋、人工智能学院师生共计50余人参加活动。

汪洋代表学校致辞，他对CCF形式化方法专委学者的到来表示热烈欢迎，并简要介绍了学校的基本情况以及CCF走进高校活动的深远意义，强调了学校十分重视形式化方法与人工智能的交叉融合及其应用。

CCF形式化方法专委秘书长吴志林对CCF形式化方法专委与江西师范大学的历史渊源进行了简要介绍，并对江西师范大学人工智能学院承办活动表示感谢。他以“RISC-V处理器Chisel设计指令集一致性验证”为主题，对其团队近年来在RISC-V处理器Chisel设计的指令集一致性形式化验证方面的工作进行介绍，并对未来进行展望。

宋富研究员以“密码的形式化验证之路：从算法安全到实现安全”为题，介绍了密码在算法和软硬件实现层面临的安全威胁，以及课题组近年来在密码算法安全、密码软硬件实现侧信道（时间、功耗、缓存）与故障注入安全的形式化验证方面取得的研究进展。

时清凯副教授以“基于分治的可靠大语言模型应用”为题，探讨大语言模型应用的一些想法，提出对“可靠使用大语言模型”的两个思路——通过分治算法缓解大语言模型幻觉及符号限制、通过可靠的结果反馈增强大语言模型领域知识——以及这两个思路在网络协议安全分析中的应用。

刘关俊教授以“鲁棒的多智能体强化学习”为题，介绍团队今年在多智能体的扰动/攻击方法以及鲁棒的强化学习上的研究成果。

孙猛教授以“人工智能×形式化方法：混沌之中，路在何方？”为题，聚焦人工智能技术与形式化方法的交叉融合，介绍其团队近期的部分相关研究成果，并探讨应对上述挑战的可能路径。

袁胜浩研究员以“面向Solana区块链eBPF指令集的完整形式语义研究”为主题，介绍了其团队首次为Solana区块链平台智能合约中使用的eBPF字节码语言提出的形式语义及语义验证框架，并展示了该语义模型在Solana eBPF虚拟机核心组件形式化中的潜在应用价值。

本次CCF形式化方法专委走进江西师范大学专场活动气氛热烈、讲者与听众互动充分，为同学们带来了创新思维视角，拓宽了同学们的学术视野，激发了同学们对形式化方法与人工智能交叉融合的浓厚兴趣。