ACM博士论文奖出炉！清华90后校友、MIT助理教授范楚楚摘获！

一年一度的 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

论文链接：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是第一个成功验证丰田动力总成控制系统和航天器会合问题的工具；也是目前唯一能够处理混合信号电路等高度非线性模型的工具。

个人主页：http://chuchu.mit.edu/

范楚楚现为 MIT 航空航天工程系的 Wilson 助理教授，也是可信赖自动化系统实验室（Reliable Autonomous Systems Lab, REASL）的负责人。她的团队致力于使用形式化方法、机器学习和控制理论等来设计、分析和验证安全的自动化系统。