Robustness Testing of Software Verifiers

Software verification tools fully automatically prove the correctness of verification tasks (i.e., programs with correctness specifications). With their increasing application on safety-critical software, the quality of such tools becomes of prime importance. This quality is typically assessed via experimental evaluation. In this paper, we present a novel approach for robustness testing of software verifiers. We consider tools to be robust if their output (for a given input task) does not change under small perturbations of the input. The core idea of our technique is to start with tasks of publicly available benchmarks and systematically apply small program transformations on them which preserve program semantics. As a consequence, the ground truth known from the benchmark (i.e., the correct outcome used as an oracle during testing) carries over to all of its perturbed versions. We experimentally evaluate robustness testing on three state-of-the-art software verifiers. To this end, we perturbate 778 tasks from the annual Competition on Software Verification via 8 transformations. Our evaluation shows that all three verifiers are non-robust, however, to different extents.