Shonan Meeting: Static analysis meets runtime verification

The goal of this meeting is to bring together the two communities of runtime verification and static analysis, to combine the robustness of static analysis and the flexibility of runtime verification. Recent years have seen, on one hand, the use of static analysis in the context of runtime verification to reduce the size of runtime models by pruning certain scenarios that are statically analyzed, on the other hand, the use of runtime verification in the context of static analysis to ease verification burden by deferring certain properties to be verified at runtime. These efforts involve both theoretical challenges of unifying different formalisms and engineering challenges of enabling different tools to communicate with each other. Another direction of research is to develop technologies for verifying software under open-world assumptions, where software is made from heterogeneous, possibly third-party, components, whose behavior and interactions cannot be fully controlled or predicted. Exhaustive static analysis is not possible for open-world software, but runtime verification can come to rescue by, for instance, verifying, at runtime, assumptions about the open world that are made during the static analysis. Discussions at the meeting will help identify research needs for combining static analysis and runtime verification. We discuss challenges for the two fields, such as verification of concurrent systems. Participants will be able to discuss technical approaches that have emerged in various related research areas and asses their applicability to the challenges we face.

Details can be found here.