图片来源：视觉
近日，最终获批立项。该项目分为5个课题，ACM公布了2020年博士论文奖得主，将建立符合我国国情的冰雪运动标准体系，清华90后女学霸、UIUC博士、MIT助理教授范楚楚荣获该奖。
近日，以冰雪运动装备滑雪板、冰刀鞋、压雪机、制冰机和造雪机为研究对象，ACM公布了2020年博士论文奖，开展关键性能参数测试技术、标准和设备的研究，清华90后女学霸范楚楚凭借着题为「安全自主性的形式方法：数据驱动的验证、综合和应用」的论文荣获该奖。
「ACM博士论文奖」每年由ACM（美国计算机协会）颁发，实现检测技术先进化和检测设备国产化，用来表彰计算机科学和计算机工程领域最佳博士论文的作者，构建质量安全性能指标评价体系。项目最终将搭建集标准研究、检验检测技术、质量安全预警、示范应用为一体的检验检测公共技术服务平台，同时者将得到2万美元的奖金。
ACM表示，形成基于冰雪运动装备制造及应用企业、检验检测机构、冰雪产业协会和相关门等多元主体的技术服务方案，范楚楚的论文在嵌入式和网络物理系统的验证有着极为重要的贡献，并在冰雪运动装备产业重点发展地区进行推广示范应用。该项目将打破国际垄断、填补国内空白，论文提出的验证技术已经可以适用于工业规模的系统。
论文推进了敏感性分析（sensitivity analysis）和符号化可达性（symbolic reachability）的理论，预期形成冰雪装备国内外标准比对分析报告1份、冰雪运动标准体系研究报告1份、新技术新方法23项；建立、行业或团体标准13项，并了相关的验证算法和软件工具（DryVR，其中4项达国际先进水平，Realsyn）。
同时，论文还为不完整模型（incomplete models）的「黑盒子」系统了第一个验证算法，该算法结合了概率近似正确（probably approximately correct, PAC）学与模拟关系（simulation relations）和不动点分析（fixed point analyses）。
其中，DryVR已被应用于包括高级驾驶辅助系统、基于神经网络的控制器、分布式机器人和医疗设备等几十个系统之中。而Realsyn则要优于现有其他方法。
90后学霸
ACM博士论文奖得主范楚楚
本次杰出博士论文奖获得者范楚楚是一名90后学霸，清华学自动化系本科2013届毕业生。
之后到美国伊利诺伊学香槟分校（UIUC），成为电气与计算机工程系的六年硕博连读研究生。
2020年秋季加入麻理工学院航天航空工程系担任助理教授，所在团队使用严格的数学方法，包括形式化方法、机器学和控制理论，以设计、分析和验证安全自主系统。
从高中开始，范楚楚学霸身份就已经「暴露无遗」，曾参加全国物理竞赛和数学竞赛并。
而在清华求学期间，也曾获三星奖学金、清华学优良毕业生称号、全国电子设计竞赛三等奖、清华学挑战杯等荣誉。
在UIUC攻读博士学位时，师从电气和计算机工程系教授Sayan Mitra，主要研究安全自主技术（如自动驾驶汽车、航天器和无人机）、控制理论、机器学、机器人技术等。
读博期间更是发表了近20篇期刊论文和会议论文。
而本次论文中提到的验证算法和软件工具C2E2、DryVR、Realsyn也是由范楚楚的。
范楚楚的学术成果喜人，也因此获得了UIUC的博士生众多奖项，2018年还获得了颁发给优秀自费留学生的奖学金。
结合范楚楚一直以来的学术背景与学术成果，这次能够获得UIUC 2020年度最佳博士论文奖也是意料之内。
荣誉奖得主
ACM除了公布2020年度杰出博士论文奖得主外，还公布了博士论文荣誉奖，者分别是Henry Corrigan-Gibbs和Ralf Jung，两人均可获得1万美元的奖金。
ACM博士论文荣誉奖得主：Henry Corrigan-Gibbs
Henry Corrigan-Gibbs是计算机科学和人工智能实验室的成员，也是MIT电气工程和计算机科学系的助理教授，获得斯坦福学计算机科学博士学位。
研究重点是计算机安全、密码学和计算机系统。
论文题为：通过拆分信任以保护隐私（Protecting Privacy by Splitting Trust）。
论文链接：https://people.csail.mit.edu/henrycg/files/academic/papers/dissertation.pdf
作者研究了如何在不了解用户的任何其他信息的情况下稳健地计算有关用户群的汇总统计数据。
该论文了一种新的概率可检查证明系统，该系统允许每个浏览器发送一个简短的零知识证明，证明其对聚合统计数据的加密贡献格式正确。同时还具有极快的证明速度。
ACM博士论文荣誉奖得主：Ralf Jung
Jung是马克思·普朗克软件系统研究所的博士后研究员，也是MIT并行和分布式操作系统组的研究员，获得萨尔学计算机科学专业的学、硕、博学位。
研究领域包括编程语言、验证、语义和类型系统。
论文题为：理解和发展Rust编程语言（Understanding and Evolving the Rust Programming Language）。
论文链接：https://people.mpi-sws.org/~jung/phd/thesis-screen.pdf
作者通过为Rust直接解释安全和不安全代码之间相互作用的语义基础，解决了缺少对Rust安全声明是否真正的严格调查的问题，为Rust的一个重要子集提供了安全性证明。
此外，论文还提供了一个平台，即使存在不安全的代码，也能用于正式验证基于类型的优化。
论文
这篇论文是范楚楚2019年在完成伊利诺伊学香槟分校电气和计算机工程专业博士学位时提交的论文。
论文链接：https://www.ideals.illinois.edu/bitstream/handle/2142/106202/FAN-DISSERTATION-2019.pdf
在现实世界中，自主系统的典型模型的验证和合成在理论上是不可知的，由于其高维度、非线性、非确定性和混合性，近似的解决方案也十分具有挑战性。
为了应对这些挑战，论文提出了：
通过非线性混合系统的可达性分析进行数据驱动的算法验证；
干扰下的高维线性系统的控制器合成。
在理论方面，论文提出的技术具有稳定性、精确性和相对完整性的保证。
在实验方面，论文提出的技术可以成功地应用于一系列具有挑战性的问题，包括首次验证的发动机控制模型、卫星控制系统、自动驾驶和基于高级辅助驾驶系统（ADAS）的操作。
论文贡献
1. 通过对非线性混合系统和非线性过渡系统的可达性分析，了一种数据驱动的安全验证算法，从而推进了网络物理系统（cyber-physical systems, CPS）的验证。
数据驱动算法在非线性系统的数据使用方面可以实现最优，并且成倍地减少了非线性过渡系统所需搜索的次数。从而能够验证难以解决的型模型。
2. 提出了第一个用于验证现实世界中没有精确数学模型的网络物理系统框架。其关键是将这些系统视为带有「黑盒」模拟器的「白盒」自动机。。
因此，验证方法可以将自动机上的最坏情况的推理与黑盒上的概率推理结合起来。
3. 提出了一种极地提高有干扰的型线性系统的控制合成效率的算法。该算法通过无需量化的线性计算简化合成问题，并利用SMT求解器，实现了可扩展性。
此外，作者还了相关的软件工具：C2E2（混合系统的验证）、DryVR（黑盒组件的系统验证）和RealSyn（用于整体）。
其中，C2E2是第一个成功验证丰田动力总成控制系统和航天器会合问题的工具；也是目前唯一能够处理混合信号电路等高度非线性模型的工具。
参考资料：https://awards.acm.org/about/2020-doctoral-dissertation
免责声明：文中图片均来源于网络，如有版权问题请联系我们进行删除！
