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.