SHF: Small: Scalable and Maximal Predictive Runtime Verification for Concurrent Software

多核处理器的使用日益广泛，其计算能力只能通过并发软件来释放，这使得软件缺陷或错误变得更加常见，检测和修复也更加劳动密集。 验证是一种新的分析方法，它从运行的系统中提取信息，并使用它来检测并可能对所观察到的满足或违反某些属性的行为做出反应。 形式化验证具有很好的可扩展性，避免了传统形式化验证技术的复杂性。在这个项目中开发的技术将导致强大的生产质量的软件，提供一个可扩展的替代正式验证，提供了许多相同的保证安全性和security.This项目的目的是开发一个可扩展的预测运行时验证frameworkfor并发software。 相对于现有技术的主要技术进步是，它不仅在错误在运行时发生时检测错误，而且能够在它们实际出现之前预测一般的安全和安全属性违反，通过采取由用户定义的适当动作来防止不良行为的发生。 该项目建立在一个健全的和最大的因果关系模型，从而提供了可证明的最大可能的预测能力，对观察到的痕迹，没有误报。 这项工作的核心研究洞察力是探索并发的最大因果关系与自动约束求解，这已经被研究了几十年，并且越来越强大。

The increasingly widespread use of multicore processors, whose computing powercan only be unleashed by concurrent software, makes software defects, or bugs,become more common and labor-intensive to detect and repair. Runtime verificationis a novel analysis approach that extracts information from a running system anduses it to detect and possibly react to observed behaviors satisfying or violatingcertain properties. Runtime verification scales well and avoids the complexity oftraditional formal verification techniques. The techniques developed in this project will lead to robust production quality software by providing a scalable alternative to formal verification that provides many of the same guarantees for safety and security.This project aims to develop a scalable predictive runtime verification frameworkfor concurrent software. A major technical advancement over prior art is that itnot only detects errors when they occur at runtime, but is able to predict generalsecurity and safety property violations before they actually surface, preventingbad behaviors from happening by taking proper actions defined by the users. Thisproject builds upon a sound and maximal causal model, hereby providing the provablymaximum possible prediction power on the observed trace with no false alarms. Thecore research insight of this work is to explore the maximal causality of concurrencywith automated constraint solving, which has been studied for decades and is becomingincreasingly powerful.