清华90后校友范楚楚获ACM博士论文奖，Rust社区Ralf

　　机器之心报道
　　机器之心编辑部
　　又一位清华校友获得ACM博士论文奖
　　一年一度的ACM博士论文奖今日发布，来自MIT的助理教授范楚楚因对嵌入式和网络物理系统的验证及其在工业规模自动化系统中的应用的贡献而获得了ACM的2020年博士论文奖。荣誉提名奖授予麻省理工学院的HenryCorriganGibbs和马克斯普朗克软件系统研究所、麻省理工学院的RalfJung。
　　该奖项每年颁发一次，旨在奖励计算机科学和工程领域最优秀的博士论文。今年的获奖者将在10月23日于旧金山举行的典礼上获颁奖项。
　　2020年ACM最佳博士论文奖
　　范楚楚荣获2020年ACM最佳博士论文奖，她的获奖论文为2019年从UIUC获得博士学位的论文，论文题目《FormalMethodsforSafeAutonomy：DataDrivenVerification，Synthesis，andApplications》。获奖理由：为嵌入式与信息物理系统的验证做出了奠基性贡献，且展示了该技术应用于工业系统的可能性。
　　论文地址：https：www。ideals。illinois。eduhandle2142106202
　　范楚楚的论文还推动了灵敏度分析和符号可达性理论的发展；开发了一系列验证算法和软件工具（DryVR，Realsyn）；展示了验证技术在工业规模自动系统中的应用。
　　本文提出的算法是第一个基于灵敏度分析的、可应用于非线性混合系统有界验证的数据驱动算法。这一工作在工业规模问题上的开创性示范表明，验证技术是可以规模化的。目前这项灵敏度分析已经获得了专利，并开始进入商业化实践。
　　范楚楚还开发了第一个用不完整模型来验证黑盒子系统的算法，该系统结合了概率近似正确（PAC）学习、模拟关系与定点分析。这项工作产生了一个工具DryVR，已经应用于几十种系统，包括先进的驾驶辅助系统、基于神经网络的控制器、分布式机器人与医疗设备等。
　　另外，范楚楚提出的算法在非线性车辆模型系统的合成控制器中具有广泛的应用前景。本文提出的RealSyn方法优于其他算法，为自动驾驶汽车实时运动规划算法铺平了道路。
　　个人主页：http：chuchu。mit。edu
　　范楚楚现为MIT航空航天工程系的Wilson助理教授，也是可信赖自动化系统实验室（ReliableAutonomousSystemsLab，REASL）的负责人。她的团队致力于使用形式化方法、机器学习和控制理论等来设计、分析和验证安全的自动化系统。
　　2009至2013年，她本科就读于清华大学自动化系，并被选为优秀毕业生。本科毕业后前往伊利诺伊大学香槟分校（UIUC）攻读博士学位，并于2019年顺利拿到计算机工程博士学位。她的主要研究兴趣在于安全自动化系统、信息物理系统、形式化方法、控制理论、机器学习、强化学习和机器人技术等。
　　博士期间，她不仅发表了多篇期刊和会议论文，还荣获了UIUCCSL学生论文奖、UIUCRobertT。Chien纪念奖等多个奖项。
　　博士毕业后，她又考取了加州理工学院的博士后研究员，并于2020年8月正式入职MIT，担任航空航天工程系的助理教授。
　　2020ACM博士论文荣誉提名奖
　　2020年ACM博士论文奖的荣誉提名授予了HenryCorriganGibbs和RalfJung。
　　CorriganGibbs获得提名的博士论文为《ProtectingPrivacybySplittingTrust》，这项研究借助理论与实践相结合的技术改善了互联网用户隐私问题。他提出了一种新型的概率可验证明（PCP）系统，然后应用这种技术开发了可扩展、满足实际行业需求的Prio系统。Prio已经部署在包括Mozilla在内的几家大公司中，自2019年底以来，它一直在夜间版本的火狐浏览器中发挥作用，这是有史以来最大的PCP部署。
　　论文地址：https：people。csail。mit。eduhenrycgfilesacademicpapersdissertation。pdf
　　CorriganGibbs的论文研究了如何在不了解有关用户的任何其他信息的情况下，有效计算有关用户群的聚合统计数据。例如，该论文介绍了一种工具，使Mozilla能够测量有多少火狐用户遇到了某种网络跟踪器，而无需了解是哪些用户遇到了该跟踪器或遇到的原因。这项研究开发了一种新的概率可验证明系统，该系统允许每个浏览器发送一个简短的零知识证明，证明其对聚合统计数据的加密贡献格式正确。论文的关键创新是验证证明的速度非常快。
　　CorriganGibbs是MIT电气工程和计算机科学系的助理教授，他也是计算机科学和人工智能实验室的成员。他的研究重点是计算机安全、密码学和计算机系统。此前，CorriganGibbs在斯坦福大学获得计算机科学博士学位。
　　RalfJung的博士论文为《UnderstandingandEvolvingtheRustProgrammingLanguage（https：people。mpisws。orgjungphdthesisscreen。pdf）》，该论文为Rust语言的安全系统编程奠定了第一个正式的基础。
　　自从2010年Mozilla开发Rust以来，它在整个行业中越来越受欢迎。Rust解决了语言设计中一个长期存在的问题：如何平衡安全性和控制。与C一样，Rust为程序员提供了对系统资源的低级控制。不同的是，Rust采用了强大的基于所有权的系统来静态确保安全，从而不会出现内存访问错误、数据竞争等安全漏洞。
　　然而，在Jung的论文之前，没有严格调查表明Rust的安全声明是否真的成立，并且由于Rust库中广泛使用unsafeescapehatches，这些声明就很难评估。
　　https：people。mpisws。orgjungphdthesisscreen。pdf
　　在他的博士论文中，Jung通过为Rust开发直接解释安全和不安全代码之间相互作用的语义基础，来解决这一挑战。在这些基础上，Jung为Rust的一个重要子集提供了安全性证明。此外，该证明在自动证明助手Coq中被形式化，因此其正确性得到保证。此外，Jung提供了一个平台，即使存在不安全代码的情况下也可用于正式验证基于类型的优化。
　　通过Jung的领导和对Rust不安全代码指南工作组的积极参与，他的工作已经对Rust的设计产生了深远的影响，并为其未来奠定了重要的基础。
　　Jung是马克斯普朗克软件系统研究所的博士后研究员，也是MIT并行和分布式操作系统组的研究员。他的研究兴趣包括编程语言、验证、语义和类型系统。他在马克斯普朗克软件系统研究所进行了博士研究，并在萨尔大学获得了计算机科学的博士、硕士和学士学位。
　　机器之心先前也报道过2018年、2019年的博士论文奖。
　　2018年，UC伯克利博士生ChelseaFinn凭借论文《LearningtoLearnwithGradients》荣获此奖。来自微软的RyanBeckett、本科毕业于清华姚班的马腾宇获得荣誉提名。
　　2019年，毕业于特拉维夫大学的DorMinzer获得该奖项，来自微软的JakubTarnawski和出身清华姚班的吴佳俊获得荣誉提名奖。