Invited talk: Fast Runtime Verification via Slow Program Analysis
The standard problem in runtime verification is the following: given a program execution and a bug pattern, decide whether the program has that type of bug. Most practical tools solve a restricted version of the problem in which the bug pattern is fixed: Valgrind looks for buffer overruns, ThreadSanitizer looks for data races. Even for these restricted problems, efficiency is an issue: for example, it is typical for Valgrind to take ~10x more time than the given execution. To address the efficiency issue – both for practical, Valgrind-like tools and for general runtime verifiers – I propose we take as input not just the program execution and the bug pattern but also the program text. Then, we preprocess (automatically) the bug pattern and the program text, in order to minimize the amount of work done while analyzing the program execution. I will present two concrete pieces of work inspired by this vision.
Fri 19 Jul
|15:40 - 16:25|
Radu GrigoreUniversity of Kent
|16:25 - 16:55|