Collaborative Research: SHF: Medium: Ensuring Safety and Liveness of Modern Systems through Dynamic Temporal Analysis

响应式/交互式系统，如web应用程序和服务器、实时视频流软件和物联网平台，已经深入到现代世界的各个方面。已经创建了许多程序分析技术和工具来分析这些系统的重要时间属性，这些属性跨越了安全性（“不会发生什么坏事”）和活动性（“最终会发生好事”）。不幸的是，现代静态分析在处理复杂的程序语义方面仍然受到限制，这些复杂的程序语义经常出现在许多实际应用程序中：它们只支持简单的属性，产生误报，或者不能扩展到大型程序。最近的动态或“数据驱动”方法解决了静态分析的几个缺点，以便更有效地分析更复杂的程序属性，但有时会产生不正确的结果。该项目的新颖之处在于静态和动态方法的理论和实践集成，以分析、定位和修复反应/交互系统的时间方面。该项目的影响是新理论和算法的发展，产生了先进的方法来确保当今反应/交互软件的安全性/活动性。今天的软件涉及复杂的非线性行为、堆操作和高阶特性。该项目使用动态分析来推断这些程序的表达属性，而使用静态验证来验证这些推断的属性。此外，静态验证和动态学习相互通知和支持彼此的力量，允许安全性/活动性分析，甚至是故障的定位和时间缺陷的综合修复。正在开发的方法包含在将公开发布的越来越多的自动化工具集合中。研究结果被用于开发新的课程，高级设计项目，以及编程语言和软件工程的交互式Jupyter书籍。该项目通过几项举措扩大了参与范围，目标是来自调查人员所在社区中代表性不足群体的初高中学生和本科生。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Reactive/interactive systems such as web applications and servers, real-time video streaming software, and IoT platforms are deeply embedded into all aspects of the modern world. Many program-analysis techniques and tools have been created to analyze important temporal properties of these systems that span both safety ("nothing bad will happen") and liveness ("something good eventually happens"). Unfortunately, modern static analyses are still limited in handling complex program semantics that often appear in many real-world applications: they support only simple properties, produce false positives, or do not scale to large programs. Recent dynamic or "data-driven" approaches address several shortcomings of static analyses to analyze more complex program properties more efficiently, yet sometimes yield incorrect results. The project's novelties are the theoretical and practical integration of static and dynamic approaches to analyze, localize, and repair temporal aspects of reactive/interactive systems. The project's impacts are the development of new theories and algorithms, giving rise to advanced methods for ensuring the safety/liveness of today's reactive/interactive software.Today's software involves complex non-linear behavior, heap manipulations, and higher-order features. The project's use of dynamic analysis enables inference of expressive properties of these programs, while the use of static verification allows for validation of those inferred properties. Furthermore, static verification and dynamic learning mutually inform and bolster the power of each other, allowing for safety/liveness analyses, and even for the localization of faults and synthesis of repairs for temporal defects. The methods being developed are embodied in a growing collection of automated tools to be released publicly. The results of the research are used to develop new courses, senior design projects, and an interactive Jupyter book in programming languages and software engineering. The project broadens participation through several initiatives, aimed at middle/high school students and undergraduate students from underrepresented groups in the investigators' local communities.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.