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.
Mon 11 SepDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
15:30 - 17:00 | |||
15:30 20mTalk | Timeout Prediction for Software Analyses [Workshop] CPAchecker Nicola Thoben University of Oldenburg | ||
15:50 20mTalk | Real-World Software Verification with CPAchecker [Workshop] CPAchecker Thomas Lemberger LMU Munich | ||
16:10 20mTalk | Using CPAchecker in Teaching [Workshop] CPAchecker Jan Haltermann University of Oldenburg File Attached | ||
16:30 20mTalk | Handling Flaky Regression Tests in CPAchecker [Workshop] CPAchecker Philipp Wendler LMU Munich |