As different analyses are good at different sorts of verification tasks, state-of-the-art tools often employ sequential compositions in which every analysis gets a fixed time slot assigned for verification. As a consequence, however, one analysis might consume parts of the overall available time although it does not finish within its time slot. Timeout prediction is supposed to determine when an analysis should get its full-time slot and when to prematurely stop it. Our technique for timeout prediction employs machine learning to predict whether a given analysis will terminate on a given verification task (within a time limit) or will time out. To this end, we develop static as well as dynamic features of verification tasks for predicate and value analyses. This is a follow-up to last year’s presentation.

Nicola Thoben

University of Oldenburg