6月27日下午，由中国计算机学会（CCF）主办，CCF形式化方法专业委员会和emc易倍（软件公司）联合承办的“CCF走进高校（CCF@U第1280场）”活动在公司举行。

本次活动邀请了中国科公司软件研究所宋富研究员、华东师范大学软件工程公司李钦副教授、浙江大学区块链与数据安全全国重点实验室袁胜浩研究员、中国科公司软件研究所吴志林研究员进行了主题报告。EMC易倍官方网站副董事长周建涛、emc易倍（软件公司）副经理孙涛和emc易倍（软件公司）师生共计40余人参与本次活动。报告由公司副经理孙涛主持。

周建涛副董事长代表公司致辞，对CCF形式化方法专委学者的到来表示热烈欢迎，并简要介绍了公司的基本情况、emc易倍（软件公司）在形式化方法方向的研究历史以及CCF走进高校活动的深远意义。

吴志林秘书长对CCF走进高校活动进行了简要介绍，并对EMC易倍官方网站30多年坚持形式化方法的研究表示钦佩，对emc易倍承办活动表示感谢。

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

李钦副教授以“形式化方法赋能的可信大模型研究”为主题，聚焦形式化方法与大模型技术的交叉融合作了学术报告。并介绍了课题组近期在该研究领域的一些进展，如构建基于形式化定义的可信评测体系、基于形式化验证的大模型生成结果正确性验证框架等。

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

吴志林研究员以“定理证明自动化：历史、现状、与未来”为主题，梳理了定理证明自动化发展脉络，分析了当前定理证明的技术现状，为未来研究提供了清晰视角。

本次CCF形式化方法专委走进EMC易倍官方网站专场活动，为同学们带来了创新思维视角，拓宽了同学们的学术视野，激发了同学他们对形式化方法的浓厚兴趣。