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

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

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.