SPLASH 会议徽标

近期，国际计算机学会 (ACM) 举办的 2024年国际系统、程序、语言和应用程序大会 (The ACM SIGPLAN International Conference on Systems, Programming, Languages and Applications: Software for Humanity (SPLASH))在美国加州帕萨迪纳落下帷幕。在会议期间举办的ACM学生研究竞赛 (Student Research Competition, SRC)中，致远学院首届约翰·霍普克罗夫特班2021级本科生钟有为展示了其关于零知识虚拟机形式化验证的参数化框架的研究工作“A Parameterized Framework for the Formal Verification of Zero-Knowledge Virtual Machines”，并荣获本科生组第二名。

钟有为获奖证书

论文首次提出了一种参数化的为零知识虚拟机进行形式化验证的框架，并首次形式化了零知识虚拟机的密码学性质。这一研究受到评审专家的高度评价，认为其非常有趣且很有意义。

钟有为在 SPLASH 2024 上演讲

ACM SIGPLAN SPLASH大会为计算机系统与程序语言领域的年度顶级国际会议之一，SPLASH 中的主要部分OOPSLA 是中国计算机学会所推荐的 A类会议。会议主要由学术报告和问题研讨等活动组成。ACM 学生研究竞赛 (SRC) 为本科生和研究生提供了一个专属的论坛，让他们有机会在 ACM主办的知名会议上向评委和与会者展示自己的原创研究成果，并有机会参与计算机科学研究社区活动。

该竞赛还为学生提供了与本领域专家讨论研究、获得反馈以及提高交流和建立学术网络等技能的机会。一般来说，会前参与者需提交一篇短文并经过该会议SRC程序委员会的专家评审。被录取文章的作者会被邀请参与会议并展示其工作，相关文章会被收录至该会议的论文集中。海报展示和演讲属于SRC竞赛的现场评比部分；会议中评委专家根据研究工作的开展情况和现场演示效果评选前三名并给以奖励，获本科生组和研究生组第一名的工作还将进入参评ACM SRC Grand Final 大奖。

钟有为（左一）在 SPLASH 2024 期间参与学生志愿者的合照

2023年4月起，钟有为在约翰·霍普克罗夫特中心曹钦翔副教授和计算机系助理教授胡云聪等老师的指导下开始了对零知识虚拟机进行形式化验证的研究。在曹老师的支持和指导下，钟有为独立完成了零知识以太坊虚拟机中约束生成算法的正确性证明，并在交互式定理证明器Coq中实现了该证明。

2024年初，钟有为进一步自主完成了参数化的零知识虚拟机验证框架的设计，并在Coq 中实现了该设计，最后在同电子信息与电气工程学院博士生的合作下，在 Coq中基于原始证明重写了参数化的约束生成算法的正确性证明，总结初步成果并提交论文到ACM SPLASH SRC，由 SRC委员会评审并获得录用。

钟有为（中）参加上海交通大学-清华大学-北京大学“成长伙伴”2023年计算机科学国际暑期学校

作为唯一一名来自中国高校的SPLASH 2024 SRC入选者，钟有为应ACM邀请与其他15位来自美国、德国等的入选者参加SPLASH 2024大会，继续进行 SRC的现场展示环节竞赛。最终，钟有为摘得本科生组第二名，获得ACM颁发的奖状及奖金奖励。

在曹钦翔、胡云聪等指导老师的悉心培养下，钟有为不仅展现了深厚的科研能力，更在海报展示和答辩中从容应对评委提问，展现了对相关领域的充分了解，表现优异。钟有为目前在耶鲁大学访问，在Ruzica Piskac教授的指导下开展科研实习活动，未来将继续致力于探索形式化验证、编程语言和密码学领域，为学术研究和产业发展贡献力量。