Software verification tools automatically prove the correctness of programs with respect to user supplied specifications. Today, such tools implement a range of different types of analyses. As different analyses are good at different sorts of verification tasks, state-of-the-art tools often employ sequential compositions of analyses 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.

In this paper, we propose timeout prediction as a way 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 and analyses. Values of static features can be statically determined for tasks; dynamic features are determined while an analysis is already running. Our experimental evaluation shows that we can predict timeouts with a high accuracy.