社区|清华90后校友、MIT助理教授范楚楚ACM博士论文奖，Rust社区Ralf Jung荣誉提名_Realsyn|系统|论文|Henry|

机器之心报道
机器之心编辑部

又一位清华校友获得ACM 博士论文奖

社区|清华90后校友、MIT助理教授范楚楚ACM博士论文奖，Rust社区Ralf Jung荣誉提名

文章图片

一年一度的 ACM 博士论文奖今日发布，来自 MIT 的助理教授范楚楚因对嵌入式和网络物理系统的验证及其在工业规模自动化系统中的应用的贡献而获得了 ACM 的 2020 年博士论文奖。荣誉提名奖授予麻省理工学院的 Henry Corrigan-Gibbs 和马克斯普朗克软件系统研究所、麻省理工学院的 Ralf Jung 。
该奖项每年颁发一次，旨在奖励计算机科学和工程领域最优秀的博士论文。今年的获奖者将在 10 月 23 日于旧金山举行的典礼上获颁奖项。
2020 年 ACM 最佳博士论文奖
范楚楚荣获 2020 年 ACM 最佳博士论文奖，她的获奖论文为 2019 年从 UIUC 获得博士学位的论文，论文题目《Formal Methods for Safe Autonomy: Data-Driven Verification, Synthesis, and Applications》。获奖理由：为嵌入式与信息物理系统的验证做出了奠基性贡献，且展示了该技术应用于工业系统的可能性。

文章图片

论文地址：https://www.ideals.illinois.edu/handle/2142/106202
范楚楚的论文还推动了灵敏度分析和符号可达性理论的发展；开发了一系列验证算法和软件工具（DryVR, Realsyn）；展示了验证技术在工业规模自动系统中的应用。
本文提出的算法是第一个基于灵敏度分析的、可应用于非线性混合系统有界验证的数据驱动算法。这一工作在工业规模问题上的开创性示范表明，验证技术是可以规模化的。目前这项灵敏度分析已经获得了专利，并开始进入商业化实践。
范楚楚还开发了第一个用不完整模型来验证「黑盒子」系统的算法，该系统结合了概率近似正确（PAC）学习、模拟关系与定点分析。这项工作产生了一个工具 DryVR ，已经应用于几十种系统，包括先进的驾驶辅助系统、基于神经网络的控制器、分布式机器人与医疗设备等。
另外，范楚楚提出的算法在非线性车辆模型系统的合成控制器中具有广泛的应用前景。本文提出的 RealSyn 方法优于其他算法，为自动驾驶汽车实时运动规划算法铺平了道路。

文章图片

个人主页：http://chuchu.mit.edu/
范楚楚现为 MIT 航空航天工程系的 Wilson 助理教授，也是可信赖自动化系统实验室（Reliable Autonomous Systems Lab, REASL）的负责人。她的团队致力于使用形式化方法、机器学习和控制理论等来设计、分析和验证安全的自动化系统。
2009 至 2013 年，她本科就读于清华大学自动化系，并被选为优秀毕业生。本科毕业后前往伊利诺伊大学香槟分校（UIUC）攻读博士学位，并于 2019 年顺利拿到计算机工程博士学位。她的主要研究兴趣在于安全自动化系统、信息物理系统、形式化方法、控制理论、机器学习、强化学习和机器人技术等。

文章图片

博士期间，她不仅发表了多篇期刊和会议论文，还荣获了 UIUC CSL 学生论文奖、UIUC Robert T. Chien 纪念奖等多个奖项。

文章图片

博士毕业后，她又考取了加州理工学院的博士后研究员，并于 2020 年 8 月正式入职 MIT ，担任航空航天工程系的助理教授。

文章图片

2020 ACM 博士论文荣誉提名奖
2020 年 ACM 博士论文奖的荣誉提名授予了 Henry Corrigan-Gibbs 和 Ralf Jung 。

文章图片

Corrigan-Gibbs 获得提名的博士论文为《Protecting Privacy by Splitting Trust》，这项研究借助理论与实践相结合的技术改善了互联网用户隐私问题。他提出了一种新型的概率可验证明 (PCP)系统，然后应用这种技术开发了可扩展、满足实际行业需求的 Prio 系统。 Prio 已经部署在包括 Mozilla 在内的几家大公司中，自 2019 年底以来，它一直在夜间版本的火狐浏览器中发挥作用，这是有史以来最大的 PCP 部署。

文章图片

论文地址：https://people.csail.mit.edu/henrycg/files/academic/papers/dissertation.pdf
Corrigan-Gibbs 的论文研究了如何在不了解有关用户的任何其他信息的情况下，有效计算有关用户群的聚合统计数据。例如，该论文介绍了一种工具，使 Mozilla 能够测量有多少火狐用户遇到了某种网络跟踪器，而无需了解是哪些用户遇到了该跟踪器或遇到的原因。这项研究开发了一种新的概率可验证明系统，该系统允许每个浏览器发送一个简短的零知识证明，证明其对聚合统计数据的加密贡献格式正确。论文的关键创新是验证证明的速度非常快。
Corrigan-Gibbs 是 MIT 电气工程和计算机科学系的助理教授，他也是计算机科学和人工智能实验室的成员。他的研究重点是计算机安全、密码学和计算机系统。此前， Corrigan-Gibbs 在斯坦福大学获得计算机科学博士学位。
Ralf Jung 的博士论文为《Understanding and Evolving the Rust Programming Language (https://people.mpi-sws.org/~jung/phd/thesis-screen.pdf)》，该论文为 Rust 语言的安全系统编程奠定了第一个正式的基础。
【社区|清华90后校友、MIT助理教授范楚楚ACM博士论文奖，Rust社区Ralf Jung荣誉提名】

文章图片

自从 2010 年 Mozilla 开发 Rust 以来，它在整个行业中越来越受欢迎。 Rust 解决了语言设计中一个长期存在的问题：如何平衡安全性和控制。与 C++ 一样， Rust 为程序员提供了对系统资源的低级控制。不同的是， Rust 采用了强大的 “基于所有权” 的系统来静态确保安全，从而不会出现内存访问错误、数据竞争等安全漏洞。
然而，在 Jung 的论文之前，没有严格调查表明 Rust 的安全声明是否真的成立，并且由于 Rust 库中广泛使用“unsafe escape hatches” ，这些声明就很难评估。

文章图片

https://people.mpi-sws.org/~jung/phd/thesis-screen.pdf
在他的博士论文中， Jung 通过为 Rust 开发直接解释安全和不安全代码之间相互作用的语义基础，来解决这一挑战。在这些基础上， Jung 为 Rust 的一个重要子集提供了安全性证明。此外，该证明在自动证明助手 Coq 中被形式化，因此其正确性得到保证。此外， Jung 提供了一个平台，即使存在不安全代码的情况下也可用于正式验证基于类型的优化。
通过 Jung 的领导和对 Rust 不安全代码指南工作组的积极参与，他的工作已经对 Rust 的设计产生了深远的影响，并为其未来奠定了重要的基础。
Jung 是马克斯普朗克软件系统研究所的博士后研究员，也是 MIT 并行和分布式操作系统组的研究员。他的研究兴趣包括编程语言、验证、语义和类型系统。他在马克斯普朗克软件系统研究所进行了博士研究，并在萨尔大学获得了计算机科学的博士、硕士和学士学位。
机器之心先前也报道过 2018 年、2019 年的博士论文奖。
2018 年， UC 伯克利博士生 Chelsea Finn 凭借论文《Learning to Learn with Gradients》荣获此奖。来自微软的 Ryan Beckett、本科毕业于清华姚班的马腾宇获得荣誉提名。