北京大学程序设计语言研究室博士一年级学生 Dimitris Bouras（导师：Sergey Mechtaev 助理教授）获得了 国家自然科学基金优秀外

国博士生科研基金（RFEIPS）的资助，项目题为《面向验证的大语言模型：融合程序推理、符号执行与智能合约验证的混合框架》。

此次资助是在 HoarePrompt 等近期科研成果取得成功后授予的。HoarePrompt 已被 ICSE 2026 接收，提出了基于自然语言最强

后条件的程序正确性推理方法。

同时，Dimitris 也正在完成另一项重要研究 Gordian，利用大型语言模型生成的“幽灵代码”突破符号执行中的复杂逻辑炸弹问题。

这些成果表明课题组在形式化验证、符号执行与大语言模型交叉研究方向上的持续突破与创新。