近日，上海交通大学电子信息与电气工程学院长聘教轨副教授汪宇霆团队在理论计算机领域机器代码验证研究方向取得重要进展，相关成果“Automatic Generation and Validation of Instruction Encoders and Decoders”已被计算机科学理论领域顶级会议The 33rd International Conference on Computer-Aided Verification(CAV2021)接收。该研究基于汪宇霆指导的第38期上海交通大学PRP（Participation in Research Program）项目“指令编码及译码的形式化研究”。


CAV是计算机科学理论领域的顶级会议之一，也是中国计算机协会（CCF）推荐A类会议。该会议致力于硬件和软件系统的计算机辅助形式化分析方法的理论和实践的进步，涵盖从实用的验证工具以及实现这些工具所需的算法和技术。CAV每年以中国科研机构为第一单位的论文仅2-3篇。
该团队开发了一套框架，其从精确的指令规范出发，自动生成编码器和译码器以及它们的一致性证明，从逻辑层面完整保障了编码译码过程的正确性。并成功将该框架应用于x86指令集的一个关键子集。
该工作解决了如何自动生成一致的、经过验证的编码器和译码器这一重要开放问题，不仅为操作机器代码的可信软件的进一步发展扫清了关键障碍，且对推动形式化指令集（Formalized Instruction Set Architectures）研究的进步有着重大意义。