This report describes the 2017 Competition on Software Verification (SV-COMP), the 6^ th
edition of the annual thorough comparative evaluation of fully-automatic software verifiers …

There are many approaches for automated software verification, but they are either
imprecise, do not scale well to large systems, or do not sufficiently leverage parallelization …

The research community made enormous progress in the past years in develo**
algorithms for verifying software, as shown by international competitions. Unfortunately, the …

Algorithm selection is the task of choosing an algorithm from a given set of candidate
algorithms when faced with a particular problem instance. Algorithm selection via machine …

Despite recent advances, software verification remains challenging. To solve hard
verification tasks, we need to leverage not just one but several different verifiers employing …

Sequential emulation is a semantics-based technique to automatically reduce property
checking of distributed systems to the analysis of sequential programs. An automated …

Symbolic computation is an important approach in automated program analysis. Most state-
of-the-art tools perform symbolic computation as interpreters and directly maintain symbolic …

The fifth version of Symbiotic significantly improves instrumentation capabilities that the tool
uses to participate in the category MemSafety. It leverages an extended pointer analysis re …

Symbiotic 7 brings improvements in all parts of the tool. In particular, we integrated the
advanced shape analysis implemented in Predator to our instrumentation process for …

Whenever a new software-verification technique is developed, additional effort is necessary
to extend the new program analysis to an interprocedural one, such that it supports recursive …