Execution-Based Validation of Violation Witnesses

Dirk Beyer, Matthias Dangl, Thomas Lemberger, and Michael Tautschnig

Download Paper


The research community made enormous progress in the past years in developing algorithms for verifying software, as shown by verification competitions (SV-COMP). However, the ultimate goal is to design certifying algorithms, which produce for a given input not only the output but in addition a witness. This makes it possible to validate that the output is a correct solution for the input problem. The advantage of certifying algorithms is that the validation of the result is —thanks to the witness— easier than the computation of the result. Unfortunately, the transfer to industry is slow, one of the reasons being that some verifiers report a considerable number of false alarms. The verification community works towards this ultimate goal using exchangeable violation witnesses, i.e., an independent validator can be used to check whether the produced witness indeed represents a bug. This reduces the required trust base from the complex verification tool to a validator that may be less complex, and thus, more easily trustable. But existing witness validators are based on model-checking technology — which does not solve the problem of reducing the trust base. To close this gap, we present a simple concept that is based on program execution: We extend witness validation by generating a test vector from an error path that is reconstructed from the witness. Then, we generate a test harness (similar to unit-test code) that can be compiled and linked together with the original program. We then run the executable program in an isolating container. If the execution violates the specification (similar to runtime verification) we confirm that the witness indeed represents a bug. This method reduces the trust base to the execution system, which seems appropriate for avoiding false alarms. To show feasibility and practicality, we implemented execution-based witness validation in two completely independent analysis frameworks, and performed a large experimental study.

Supplementary Data

We performed an extensive experimental evaluation to show the potential and feasibility of our approach. We used 21 tools that participated in the 6th International Competition on Software Verification (SV-COMP'17) to verify tasks from the version (423cf8c) of the SV-COMP benchmark set. Every of these tools produced a violation witness for each property violation it found. To receive more high-quality witnesses, we also used testification to refine these witnesses, where possible. Based on the produced witnesses, i.e., the full set of produced violation witnesses in addition to the set of successfully refined violation witnesses, we compared the two execution-based validators CPA-witness2test and FShell-witness2test to the two validators CPAchecker and Ultimate Automizer, both of which are based on model-checking techniques.

The 21 tools used for witness creation were used in the respective versions they were submitted to SV-COMP'17 to. There archives are available here. Regarding witness validators, CPAchecker and CPA-witness2test were used in revision 24473 of the trunk. FShell-witness2test was used in revision 2a76669f from the test-gen branch. Ultimate automizer was used in release v0.1.8.

Raw witnesses Refined witnesses
Witness Validator
CPAchecker HTML Table CSV Table Validation Log Files
Ultimate Automizer HTML Table CSV Table Validation Log Files
CPA-witness2test HTML Table CSV Table Validation Log Files Created harnesses
FShell-witness2test HTML Table CSV Table Validation Log Files Created harnesses