Trustworthy Software Project Generation: A Case Study with an Interactive Theorem Prover
JAWs 2: Journal Ahead Workshop at ASE 2026 · 2026年10月
ACM杰出会员, IFIP WG 2.4成员，IEEE和CCF会员
办公室：北京大学燕园校区理科一号楼1431房间 / 北京大学昌平新校区文德楼447
电子邮件：xiongyf@pku.edu.cn
电话：010-62757008-12
新闻
更多新闻 →我成功晋升为北京大学长聘教授。感谢一路走来帮助过我的同学、老师、同行！
Mining Tactics for Automated Theorem Proving被ASE 2026接收。这是我们新项目的第一篇论文，该项目用大模型的智能来提升符号证明工具的能力。我们相信，与大模型相比，符号方法更适合处理符号问题，但迄今为止投入的人类智能还不足以发现最合适的符号方法，因此我们利用大模型来继续开发。通过数据驱动的大模型策略生成，我们的方法仅用一个小型训练集就将CoqHammer提升了20%以上。
SemOpt: LLM-Driven Code Optimization via Rule-Based Analysis被TOSEM 2026接收。本文中，我们使用大语言模型从历史提交中挖掘优化策略，并将其形式化为semgrep规则，进而利用这些规则在大型软件项目中挖掘优化机会来引导大语言模型进行优化。我们成功优化了多个经过人类专家多年优化的热门软件项目，其中部分生成的补丁已被开发者采纳。
Reducing Cost of LLM Agents with Trajectory Reduction被FSE 2026录用。本文提出了首个降低大模型智能体对话长度的通用方法，通过去除推理轨迹中不必要的内容并保留智能体的推理能力来降低使用成本。
Mining Tactics for Automated Theorem Proving
ASE'26: 41th IEEE/ACM International Conference on Automated Software Engineering · 2026年10月
SemOpt: LLM-Driven Code Optimization via Rule-Based Analysis
TOSEM: ACM Transactions on Software Engineering and Methodology · 2026年7月
Reducing Cost of LLM Agents with Trajectory Reduction
FSE'26: The ACM International Conference on the Foundations of Software Engineering · 2026年7月
HoarePrompt: Structural Reasoning About Program Correctness in Natural Language
ICSE'26: 48th IEEE/ACM International Conference on Software Engineering · 2026年5月
✦ ACM SIGSOFT杰出论文奖
教育与工作经历
学术和院系服务
更多 →2027
领域主席 · ICSE 2028
2027
领域主席 · ISSTA 2027
2026
程序委员会主席 · 第一届CCF程序设计语言会议
2026
副主席 · PLDI 2027
2026-2028
副主编 · IEEE Transactions on Software Engineering
2026
程序委员会委员 · POPL 2027
2026
程序委员会委员 · ICSE 2027
2026
副主席 · OOPSLA 2026