The CPAchecker is successfully used in verification and has a lot of active developers around the world. Due to its configurable design, it offers many possibilities for developing new analyses. We use the CPAchecker in a Bachelor and a Master course to enrich theoretical lectures with practical hands-on exercises. In this talk, I will give an overview of our usage within the lecture as well as a personal experience report.
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.
The CPAchecker is successfully used in verification and has a lot of active developers around the world. Due to its configurable design, it offers many possibilities for developing new analyses. We use the CPAchecker in a Bachelor and a Master course to enrich theoretical lectures with practical hands-on exercises. In this talk, I will give an overview of our usage within the lecture as well as a personal experience report.
Flaky tests that non-deterministically pass or fail are a major impediment to regression testing. Existing work on identifying flaky tests is mostly based on test re-executions, which may be a feasible solution for short-running unit tests, but can become prohibitively expensive for long-running integration and system tests. To alleviate the problem, we propose a novel heuristic for identifying flaky test results by analyzing run-length encodings of regression test histories. For flagging tests as flaky, the proposed heuristic solely requires knowledge about previous test results and neither requires test re-executions nor expensive model fitting. We apply this heuristic in the context of the CPAchecker project, which heavily relies on integration tests for regression testing.
