CAREER: Robustness Analysis of Uncertain Programs: Theory, Algorithms, and Tools

这项研究计划将开发数学技术，以自动证明计算机程序在不确定条件下运行的健壮性。其目的是弥合健壮性控制理论研究与程序语义和分析之间的差距。在信息物理系统中，传感器从物理世界获得的数据与计算交织在一起，不确定性来自不稳定的或错误的传感器数据。这样的系统需要对系统初始条件的扰动做出可预测的响应，否则它们将是不可靠的。该项目有三个主题：(1)理论：它将创建复杂数据类型上命令式程序设置中的健壮性属性的全面语义，如连续性和稳定性。(2)算法：需要分析算法来证明程序的健壮性，或者交替发现违反健壮性的行为。可扩展的轻量级分析将与精确但重量级的方法一起开发。(3)工具：这些分析将在适用于现实世界网络物理系统软件的工具中实施。

This research program will develop mathematical techniques to automatically prove the robustness of computer programs operating under uncertainty. The aim is to bridge the gap between control-theoretic studies of robustness, on the one hand, and program semantics and analysis on the other. In cyberphysical systems, where sensor-derived data from the physical world is intertwined with computations, uncertainty arises from volatile or erroneous sensor data. Such systems demand predictable responses to perturbations of the system's initial conditions, otherwise they will be unreliable. The project has three themes: (1) Theory: It will create comprehensive semantics of robustness properties such as continuity and stability in the setting of imperative programs over complex data types. (2) Algorithms: Analysis algorithms are needed to prove robustness of programs, or alternately find violations of robustness. Scalable, lightweight analyses will be developed along with precise but heavyweight methods. (3) Tools: These analyses will be implemented in tools applicable to software for real-world cyber-physical systems.