又一位清華校友獲得ACM 博士論文獎

[[411517]]

一年一度的 ACM 博士論文獎今日發(fā)布，來自 MIT 的助理教授范楚楚因對嵌入式和網絡物理系統的驗證及其在工業(yè)規(guī)模自動化系統中的應用的貢獻而獲得了 ACM 的 2020 年博士論文獎。榮譽提名獎授予麻省理工學院的 Henry Corrigan-Gibbs 和馬克斯普朗克軟件系統研究所、麻省理工學院的 Ralf Jung。

該獎項每年頒發(fā)一次，旨在獎勵計算機科學和工程領域最優(yōu)秀的博士論文。今年的獲獎者將在 10 月 23 日于舊金山舉行的典禮上獲頒獎項。

2020 年 ACM 最佳博士論文獎

范楚楚榮獲 2020 年 ACM 最佳博士論文獎，她的獲獎論文為 2019 年從 UIUC 獲得博士學位的論文，論文題目《Formal Methods for Safe Autonomy: Data-Driven Verification, Synthesis, and Applications》。獲獎理由：為嵌入式與信息物理系統的驗證做出了奠基性貢獻，且展示了該技術應用于工業(yè)系統的可能性。

論文地址：https://www.ideals.illinois.edu/handle/2142/106202

范楚楚的論文還推動了靈敏度分析和符號可達性理論的發(fā)展；開發(fā)了一系列驗證算法和軟件工具（DryVR, Realsyn）；展示了驗證技術在工業(yè)規(guī)模自動系統中的應用。

本文提出的算法是第一個基于靈敏度分析的、可應用于非線性混合系統有界驗證的數據驅動算法。這一工作在工業(yè)規(guī)模問題上的開創(chuàng)性示范表明，驗證技術是可以規(guī)?；摹Ｄ壳斑@項靈敏度分析已經獲得了專利，并開始進入商業(yè)化實踐。

范楚楚還開發(fā)了第一個用不完整模型來驗證「黑盒子」系統的算法，該系統結合了概率近似正確（PAC）學習、模擬關系與定點分析。這項工作產生了一個工具 DryVR，已經應用于幾十種系統，包括先進的駕駛輔助系統、基于神經網絡的控制器、分布式機器人與醫(yī)療設備等。

另外，范楚楚提出的算法在非線性車輛模型系統的合成控制器中具有廣泛的應用前景。本文提出的 RealSyn 方法優(yōu)于其他算法，為自動駕駛汽車實時運動規(guī)劃算法鋪平了道路。

個人主頁：http://chuchu.mit.edu/

范楚楚現為 MIT 航空航天工程系的 Wilson 助理教授，也是可信賴自動化系統實驗室（Reliable Autonomous Systems Lab, REASL）的負責人。她的團隊致力于使用形式化方法、機器學習和控制理論等來設計、分析和驗證安全的自動化系統。

2009 至 2013 年，她本科就讀于清華大學自動化系，并被選為優(yōu)秀畢業(yè)生。本科畢業(yè)后前往伊利諾伊大學香檳分校（UIUC）攻讀博士學位，并于 2019 年順利拿到計算機工程博士學位。她的主要研究興趣在于安全自動化系統、信息物理系統、形式化方法、控制理論、機器學習、強化學習和機器人技術等。

博士期間，她不僅發(fā)表了多篇期刊和會議論文，還榮獲了 UIUC CSL 學生論文獎、UIUC Robert T. Chien 紀念獎等多個獎項。

博士畢業(yè)后，她又考取了加州理工學院的博士后研究員，并于 2020 年 8 月正式入職 MIT，擔任航空航天工程系的助理教授。

2020 ACM 博士論文榮譽提名獎

2020 年 ACM 博士論文獎的榮譽提名授予了 Henry Corrigan-Gibbs 和 Ralf Jung。

Corrigan-Gibbs 獲得提名的博士論文為《Protecting Privacy by Splitting Trust》，這項研究借助理論與實踐相結合的技術改善了互聯網用戶隱私問題。他提出了一種新型的概率可驗證明 (PCP)系統，然后應用這種技術開發(fā)了可擴展、滿足實際行業(yè)需求的 Prio 系統。Prio 已經部署在包括 Mozilla 在內的幾家大公司中，自 2019 年底以來，它一直在夜間版本的 火狐瀏覽器中發(fā)揮作用，這是有史以來最大的 PCP 部署。

論文地址：https://people.csail.mit.edu/henrycg/files/academic/papers/dissertation.pdf

Corrigan-Gibbs 的論文研究了如何在不了解有關用戶的任何其他信息的情況下，有效計算有關用戶群的聚合統計數據。例如，該論文介紹了一種工具，使 Mozilla 能夠測量有多少火狐用戶遇到了某種網絡跟蹤器，而無需了解是哪些用戶遇到了該跟蹤器或遇到的原因。這項研究開發(fā)了一種新的概率可驗證明系統，該系統允許每個瀏覽器發(fā)送一個簡短的零知識證明，證明其對聚合統計數據的加密貢獻格式正確。論文的關鍵創(chuàng)新是驗證證明的速度非?？?。

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 語言的安全系統編程奠定了第一個正式的基礎。

自從 2010 年 Mozilla 開發(fā) Rust 以來，它在整個行業(yè)中越來越受歡迎。Rust 解決了語言設計中一個長期存在的問題：如何平衡安全性和控制。與 C++ 一樣，Rust 為程序員提供了對系統資源的低級控制。不同的是，Rust 采用了強大的 “基于所有權” 的系統來靜態(tài)確保安全，從而不會出現內存訪問錯誤、數據競爭等安全漏洞。

然而，在 Jung 的論文之前，沒有嚴格調查表明 Rust 的安全聲明是否真的成立，并且由于 Rust 庫中廣泛使用“unsafe escape hatches”，這些聲明就很難評估。

https://people.mpi-sws.org/~jung/phd/thesis-screen.pdf

在他的博士論文中，Jung 通過為 Rust 開發(fā)直接解釋安全和不安全代碼之間相互作用的語義基礎，來解決這一挑戰(zhàn)。在這些基礎上，Jung 為 Rust 的一個重要子集提供了安全性證明。此外，該證明在自動證明助手 Coq 中被形式化，因此其正確性得到保證。此外，Jung 提供了一個平臺，即使存在不安全代碼的情況下也可用于正式驗證基于類型的優(yōu)化。

通過 Jung 的領導和對 Rust 不安全代碼指南工作組的積極參與，他的工作已經對 Rust 的設計產生了深遠的影響，并為其未來奠定了重要的基礎。

Jung 是馬克斯普朗克軟件系統研究所的博士后研究員，也是 MIT 并行和分布式操作系統組的研究員。他的研究興趣包括編程語言、驗證、語義和類型系統。他在馬克斯普朗克軟件系統研究所進行了博士研究，并在薩爾大學獲得了計算機科學的博士、碩士和學士學位。

機器之心先前也報道過 2018 年、2019 年的博士論文獎。

2018 年，UC 伯克利博士生 Chelsea Finn 憑借論文《Learning to Learn with Gradients》榮獲此獎。來自微軟的 Ryan Beckett、本科畢業(yè)于清華姚班的馬騰宇獲得榮譽提名。

2019 年，畢業(yè)于特拉維夫大學的 Dor Minzer 獲得該獎項，來自微軟的 Jakub Tarnawski 和出身清華姚班的吳佳俊獲得榮譽提名獎。