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.
