近日，IEEE/ACM International Conference on Embedded Software（EMSOFT 2026）在西班牙巴塞罗那举行。EMSOFT是IEEE/ACM Embedded Systems Week（ESWEEK）的三大核心会议之一，是嵌入式软件领域具有重要国际影响力的顶级学术会议，被官方称为嵌入式软件前沿研究的“premier venue”。

山东大学戴鸿君教授团队的研究成果“VERA: A Formal Framework for Firmware-First RAS Verification”入选会议Journal Track，并在会议期间完成报告和海报展示。博士生杨叶倩为论文第一作者，戴鸿君教授为通讯作者，中国科学院软件研究所于佳耕为共同作者。

随着AI集群和高性能服务器规模扩大，固件承担着硬件错误收集、调度和上报等关键任务。处理不当可能导致错误丢失、重复上报、优先级反转和跨处理单元干扰，而传统测试难以穷举异步中断与多核交互形成的复杂状态空间。

针对这一问题，团队提出VERA形式化验证框架并实现RISC-V原型VeraSBI。VERA建立三层错误—事件—分发模型，定义并验证P1至P4四项安全性质，通过“初始状态—单步保持—轨迹闭包—可达状态闭包”证明其覆盖全部可达状态。此外，团队还开发、验证了健康查询、阈值控制和处理器核状态控制三类SBI接口，形成从抽象模型、机器证明、C代码契约到运行测试的完整证据链。

最终，形成的VeraSBI固件包含132个文件、17429行代码，其中RAS相关部分为22个文件、4637行代码。9个Dafny文件中的1159个断言全部通过且无遗留assume假设；9个关键C函数的560项Frama-C/WP证明目标全部完成。

此外，团队还开展了多组定向测试、模型与C实现的差分测试以及SSE状态机转换检查。结果表明，错误报告与注入场景一致，C实现与形式模型输出一致，各项状态转换均符合规约。验证过程还发现并修复了状态保护、标志校验、事件复位、pending清除和优先级比较等固件实现问题。

综上，VERA为RISC-V固件优先RAS路径建立了涵盖抽象建模、机器证明、C代码契约、差分测试和运行验证的完整证据链，为提升服务器底层错误处理机制的可信性提供了技术基础。该成果体现了博士生杨叶倩在RISC-V系统软件与形式化验证领域的长期研究积累，以及在形式验证与原型评估方面的综合研究能力。