CCF@U第1282场：CCF形式化方法专委走进江西师范大学
7月6日下午，由中国计算机学会（CCF）主办，CCF形式化方法专业委员会和江西师范大学人工智能学院(原计算机信息工程学院)联合承办的“CCF走进高校（CCF@U第1282场）”活动在江西师范大学先骕楼4218会议室举行。
本次活动邀请了中国科学院软件研究所宋富研究员、南京大学计算机学院时清凯副教授、同济大学计算机科学与技术学院刘关俊教授、北京大学数学科学学院孙猛教授、浙江大学区块链与数据安全全国重点实验室袁胜浩研究员、中国科学院软件研究所吴志林研究员做了主题报告。江西师范大学大学党委副书记汪洋、人工智能学院师生共计50余人参与本次活动。
党委副书记汪洋代表学校致辞，对CCF形式化方法专委学者的到来表示热烈欢迎，并简要介绍了学校的基本情况以及CCF走进高校活动的深远意义，强调学校十分重视形式化方法与人工智能的交叉融合及其应用。
吴志林秘书长强调在人工智能领域大模型迅猛发展的现在，形式化方法作为确保系统可靠性的核心理论工具，其战略价值愈发凸显。同时也对CCF形式化方法专委与江西师范大学的历史渊源进行了简要介绍，并对江西师范大学人工智能学院承办活动表示感谢。
宋富研究员以“密码的形式化验证之路：从算法安全到实现安全”为题，介绍了密码在算法和软硬件实现层面临的安全威胁，以及课题组近年来在密码算法安全、密码软硬件实现侧信道（时间、功耗、缓存）与故障注入安全的形式化验证方面取得的研究进展。
时清凯副教授以“基于分治的可靠大语言模型应用”为题，探讨大语言模型应用的一些想法，提出对“可靠使用大语言模型”的两个思路——通过分治算法缓解大语言模型幻觉及符号限制、通过可靠的结果反馈增强大语言模型领域知识——以及这两个思路在网络协议安全分析中的应用。
刘关俊教授以“鲁棒的多智能体强化学习”为题，介绍团队今年在多智能体的扰动/攻击方法以及鲁棒的强化学习上的研究成果。
孙猛教授以“人工智能×形式化方法：混沌之中，路在何方？”为题，聚焦人工智能技术与形式化方法的交叉融合，介绍其团队近期的部分相关研究成果，并探讨应对上述挑战的可能路径。
袁胜浩研究员以“面向Solana区块链eBPF指令集的完整形式语义研究”为主题，介绍了其团队首次为Solana区块链平台智能合约中使用的eBPF字节码语言提出的形式语义及语义验证框架，并展示了该语义模型在Solana eBPF虚拟机核心组件形式化中的潜在应用价值。
吴志林研究员以“RISC-V处理器Chisel设计指令集一致性验证”为主题，对其团队近年来在RISC-V处理器Chisel设计的指令集一致性形式化验证方面的工作进行介绍，并对未来进行展望。
本次CCF形式化方法专委走进江西师范大学专场活动气氛热烈、讲者与听众互动充分，为同学们带来了创新思维视角，拓宽了同学们的学术视野，激发了同学们对形式化方法与人工智能交叉融合的浓厚兴趣。
京公网安备 11010802032778号