This report describes the 2019 Competition on Software Verification (SV-COMP), the 8^ th
edition of a series of comparative evaluations of fully automatic software verifiers for C …

Testing is a widely used method to assess software quality. Coverage criteria and coverage
measurements are used to ensure that the constructed test suites adequately test the given …

The goal of cooperative verification is to combine verification approaches in such a way that
they work together to verify a system model. In particular, cooperative verifiers provide …

There are publications that consider the use of program slicing in software verification, but
we are aware of no publication that thoroughly evaluates the impact of program slicing on …

The paper describes a successful approach to checking computer programs for standard
memory handling errors like invalid pointer dereference or memory leaking. The approach is …

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 …

We propose a shape analysis suitable for analysis engines that perform automatic invariant
inference using an SMT solver. The proposed solution includes an abstract template domain …

Software quality is often evaluated by testing the software on an adequate test suite, eg, a
test suite achieving certain or high coverage of the software. Manually generating such test …

Testing is a widely applied technique to evaluate software quality, and coverage criteria are
often used to assess the adequacy of a generated test suite. However, manually …

We present an improved version of the memory safety verification approach implemented in
Symbiotic 5, the winner of the MemSafety category at the Competition on Software …