2018年9月3日至7日，第33届IEEE/ACM自动软件工程国际大会在法国Montpellier召开。由清华大学软件学院贺飞副教授同其博士研究生陈建辉完成的论文《基于控制流引导的程序验证SMT问题求解》（Control Flow-Guided SMT Solving for Program Verification）获得大会“杰出论文奖”（ACM SIGSOFT Distinguished Papers）。该论文针对程序验证的一阶理论可满足性判定问题（Satisfiability Modulo Theories, SMT），创新的提出了利用程序控制流信息的方法，构造程序变量偏序关系，引导SMT自动推理过程，显著提高了SMT的求解速度，改进了程序验证的效率与规模。

该论文为清华大学软件学院独立完成，论文结果在大会报告以后，得到国内外同行的广泛关注，将对程序分析与验证的学术研究产生积极影响。

IEEE/ACM自动软件工程国际会议始于1986年，是软件工程领域的3大国际顶会之一（CCF Rank A），由ACM下属的SIGSOFT组织主办，主要关注软件系统分析、设计、实现、测试、维护的自动化技术的最新研究成果。本次大会共收录了69篇长文和11篇短文，总录取率为21%，共6篇论文获杰出论文奖项。

供稿：贺飞

审核：刘璘