在山东大学智能创新研究院戴鸿君教授指导下，博士生杨叶倩在RISC-V固件形式化验证方向取得系统性突破，相关成果发表于“IEEE Transactions on Computer-Aided Design of Integrated Circuits & Systems (TCAD)”、“Journal of Systems Architecture (JSA)”、“计算机研究与发展”等权威期刊和国际会议。

SBI固件是开源RISC-V体系结构中连接硬件与操作系统的关键接口，其启动过程的正确性直接影响系统安全。然而，主流SBI固件长期依赖测试、缺乏严格数学保证。为解决该问题，杨叶倩博士提出定理证明驱动的分层形式化验证框架，研发经形式化验证的SBI固件SeSBI，并对启动流程、定时器等关键功能进行验证，成果发表于《计算机研究与发展》。

在验证过程中，其发现，SBI固件验证过程缺乏系统化组织，验证有效性难以量化评估。为解决上述问题，其进一步提出由抽象状态证明、可执行契约和数据表示检查组成的三层验证工作流，结合真实缺陷分析与受控变异实验，评估了该方法的缺陷检测能力，成果发表于《Journal of Systems Architecture》。

后续研究聚焦于RAS固件形式化验证，以保障AI推理服务的可靠性。为解决RAS固件层中可能出现的错误丢失、重复、优先级反转和跨处理单元干扰等问题，其提出基于抽象模型、Dafny机器证明和C级契约验证的形式化验证框架VERA，并在RISC-V RAS错误处理路径上完成原型实现与验证，成果发表于《IEEE Transactions on Computer-Aided Design of Integrated Circuits & Systems》。

在形式验证工具研究方面，Dafny验证超时缺乏根因信息，导致人工诊断与修复成本高昂。为此，其提出多层诊断工具DafnyDiag。该工具能够通过综合分析源代码、验证日志、Boogie中间表示和SMT查询，辅助识别超时原因并选择修复策略，成果发表于QRS 2026。

围绕固件形式化验证核心技术，杨叶倩博士已申请4项发明专利，覆盖半自动验证、多核并发验证、大语言模型辅助证明等方向。代表性专利包括“一种针对固件的半自动精化关系验证方法及系统”（CN120066931B），“一种针对RISC-V多核SBI固件的形式验证方法及系统”（CN202511556868.4），“基于大语言模型的证明搜索与策略生成方法及系统”（2026108286921）。

在学术交流方面，其多次参加RISC-V中国峰会，并在2025年RISC-V中国峰会以Poster形式展示阶段性成果。

同年，在第二届固件技术峰会上作专题报告，重点分享其在RISC-V SBI固件方面的研究成果。

综上，杨叶倩博士在RISC-V固件形式化验证领域构建了覆盖启动安全、运行时可靠性、验证工具效率以及多核并发的完整研究体系。其工作成果为RISC-V开源生态的可信计算和AI时代高可靠基础设施的发展提供支撑。