Collaborative Resaerch: SHF: Medium: Ensuring Safety and Liveness of Modern Systems through Dynamic Temporal Analysiss

Web应用程序和服务器、实时视频流软件和物联网平台等反应式/交互式系统深深嵌入到现代世界的各个方面。人们已经创建了许多程序分析技术和工具来分析这些系统的重要时间属性，这些属性涵盖安全性（“不会发生任何不好的事情”）和活跃性（“最终会发生一些好的事情”）。不幸的是，现代静态分析在处理复杂的程序语义方面仍然受到限制，这些语义经常出现在许多现实世界的应用程序中：它们只支持简单的属性，产生误报，或者不能扩展到大型程序。最近的动态或“数据驱动”的方法解决了静态分析的几个缺点，以更有效地分析更复杂的程序属性，但有时会产生不正确的结果。该项目的新颖之处是静态和动态方法的理论和实践整合，以分析，本地化和修复反应/交互系统的时间方面。该项目的影响是新的理论和算法的发展，从而产生了先进的方法，以确保今天的反应/交互式软件的安全性/活性。今天的软件涉及复杂的非线性行为，堆操作和高阶特征。该项目的动态分析的使用，使这些程序的表达属性的推断，而静态验证的使用允许验证这些推断的属性。此外，静态验证和动态学习相互通知和支持彼此的力量，允许安全/活性分析，甚至用于故障的定位和临时缺陷的修复的合成。正在开发的方法体现在越来越多的公开发布的自动化工具中。研究结果用于开发新课程，高级设计项目，以及编程语言和软件工程的交互式电子书。该项目通过多项举措扩大了参与范围，目标群体是研究者所在社区中代表性不足的初中/高中学生和本科生。该奖项反映了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.