近日，电子信息与电气工程学院约翰·霍普克罗夫特计算机科学中心长聘教轨副教授曹钦翔团队与汪宇霆团队分别在程序验证与编译器验证的研究中取得重要进展，研究成果“VST-A: A Foundationally Sound Annotation Verifier”（VST- A：保证本身可靠性的带标注程序验证工具）和“Fully Composable and Adequate Verified Compilation with Direct Refinements between Open Modules”（支持开放模块直接精化的完全可组合充分编译验证方法） 均被程序语言方向的顶级国际会议Principles of Programming Languages（POPL 2024）录用。两篇论文的第一完成单位均是上海交通大学，曹钦翔与汪宇霆分别是唯一通讯作者。

POPL是程序设计语言领域历史最久、水平最高的国际会议，也是中国计算机协会（CCF）推荐的A类会议。会议主要关注程序设计语言的基本原理和重要创新，内容涵盖程序语言设计、程序分析、程序验证、编译器技术等具体领域。截至目前，中国大陆高校和科研机构作为第一完成单位发表的POPL论文数量极少，本届POPL正式发表的论文93篇，其中大陆论文仅4篇（2020-2024五年内仅8篇）。

成果简介

VST-A: A Foundationally Sound Annotation Verifier

基于交互式定理证明的程序验证是用于验证复杂程序复杂性质（特别是程序功能正确性）的有力手段。但这一验证方法需要验证人员先使用形式化的证明语言编写证明代码，再交由验证工具检验，其中所需的人力成本极高，平均每验证1行程序代码就需要验证人员开发15-40行证明代码。因此，目前只有一些安全攸关领域关键软件的核心模块可以采用这种方式实现全覆盖、无漏报的程序验证。如何能够更为便捷地表述一段程序的功能正确性证明是该领域聚焦关注的一个重要问题。

控制流图与拆分结果

本论文首次提出了基于程序逻辑理论利用程序断言标注构造程序功能正确性证明的技术方案，并开发了VST-A验证工具用于验证C语言程序的安全性与功能正确性。这一工作在VST验证工具的基础上进一步提升了程序验证工具的自动化程度与易用性。使用VST-A时，验证人员手动编写的“证明”分为两部分，其一是以程序断言形式描述的较为简明易读的程序功能正确证明整体框架，其二是在定理证明器中编写的详细局部证明。

这一新验证技术的关键是基于程序断言将程序的控制流图拆分成为若干简单无分叉路径，曹钦翔与其团队证明，整体程序的全局功能正确性可以由这些简单控制流图路径的局部功能正确性导出，并基于后者的霍尔逻辑证明重新构造前者的霍尔逻辑证明。

论文链接：https://arxiv.org/abs/1909.00097

曹钦翔，上海交通大学长聘教轨副教授、博士生导师。2013年本科毕业于北京大学，2018年在普林斯顿大学获得博士学位，曾获上海浦江人才计划资助。曹钦翔长期从事基于定理证明的程序验证与程序逻辑研究，论文主要发表在POPL、OOPSLA、JAR等国际著名会议或期刊，其代表性工作VST程序验证工具是目前世界范围内最知名的几个程序验证工具之一。

Fully Composable and Adequate Verified Compilation with Direct Refinements between Open Modules

编译器是关键性的系统软件，任何编译漏洞都可能导致目标程序运行时出现严重错误。因此，通过形式验证确保编译器正确性是形式化方法领域受到长期关注的话题。尽管历经多年发展，现有编译器验证方法仍无法有效支持现代软件中普遍存在的异构程序模块（如不同语言编写的程序库）。这是由于它们产生的验证结果暴露了中间程序语义，导致第三方用户必须理解编译链的具体实现才能运用验证结果，严重限制了编译器验证的应用范围，并造成了极高的使用成本。