Interpretation-Based Violation Witness Validation for C: NITWIT
55
state, we deliberately stop the validation and output Unknown. We experimented
with the threshold and concluded that 1 million attempts is appropriate. By enabling this threshold, we went from 784 to 123 killed validations and lost only
25 witnesses that would otherwise have been validated, which is an acceptable
trade-off. An analysis showed that 573 of the 784 timeouts were validations of
possibly non-terminating programs, 18 for terminating and the 193 remaining
validations without specified termination
5 . The check for the threshold can be
disabled.
Processing witnesses. In some cases, software verifiers do not always produce
witnesses in exactly the correct format. For example, in GraphML it is necessary
to define attributes for the graph, nodes and edges. If a witness happens to
contain no such definitions, we supply a basic configuration that allows for its
successful parsing. By default, we also do not extensively check for correctness
of all of the graph attributes like the program hash.
Furthermore, we consider a reached error location as a proof of violation even
if the witness automaton itself does not finish in an error state. This behavior
can be changed by a compilation flag to rejection. Nevertheless, if a witness
resolves enough determinism for one execution to find an error, we think it is
sufficiently “good” for it to be a viable witness. For some programs, the variable
resolving at the start suffices to reach a violation. However, we output a special
exit code to make it clear that the witness did not in fact accept this path.
6 Conclusion
We presented the new interpretation-based violation witness validator nitwit,
that was able to validate 8 526 witnesses from a dataset of 11 533 witnesses [9]
that were produced in the ReachSafety category of the 2020 edition of SVCOMP. nitwit was able to validate 399 witnesses that have not been validated
by any other participating tool. In addition, nitwit has a small memory footprint and is mostly significantly faster than its competitors.
Data Availability Statement and Acknowledgments. nitwit is available for free
at https://github.com/moves-rwth/nitwit-validator and is licensed under the
New BSD license. The replication artifact can be found at the Zenodo repository
https://doi.org/10.5281/zenodo.3518139 [23] and the datasets analyzed during
the current study at https://doi.org/10.5281/zenodo.3630205 [8]. We thank Dirk
Beyer for very useful feedback on an earlier version of the paper and assistance
with configuring nitwit for SV-COMP 2020.
5 We know whether these programs are (non-)terminating, as they were reviewed in
SV-COMP before including them in the competition on termination analysis.
55
state, we deliberately stop the validation and output Unknown. We experimented
with the threshold and concluded that 1 million attempts is appropriate. By enabling this threshold, we went from 784 to 123 killed validations and lost only
25 witnesses that would otherwise have been validated, which is an acceptable
trade-off. An analysis showed that 573 of the 784 timeouts were validations of
possibly non-terminating programs, 18 for terminating and the 193 remaining
validations without specified termination
5 . The check for the threshold can be
disabled.
Processing witnesses. In some cases, software verifiers do not always produce
witnesses in exactly the correct format. For example, in GraphML it is necessary
to define attributes for the graph, nodes and edges. If a witness happens to
contain no such definitions, we supply a basic configuration that allows for its
successful parsing. By default, we also do not extensively check for correctness
of all of the graph attributes like the program hash.
Furthermore, we consider a reached error location as a proof of violation even
if the witness automaton itself does not finish in an error state. This behavior
can be changed by a compilation flag to rejection. Nevertheless, if a witness
resolves enough determinism for one execution to find an error, we think it is
sufficiently “good” for it to be a viable witness. For some programs, the variable
resolving at the start suffices to reach a violation. However, we output a special
exit code to make it clear that the witness did not in fact accept this path.
6 Conclusion
We presented the new interpretation-based violation witness validator nitwit,
that was able to validate 8 526 witnesses from a dataset of 11 533 witnesses [9]
that were produced in the ReachSafety category of the 2020 edition of SVCOMP. nitwit was able to validate 399 witnesses that have not been validated
by any other participating tool. In addition, nitwit has a small memory footprint and is mostly significantly faster than its competitors.
Data Availability Statement and Acknowledgments. nitwit is available for free
at https://github.com/moves-rwth/nitwit-validator and is licensed under the
New BSD license. The replication artifact can be found at the Zenodo repository
https://doi.org/10.5281/zenodo.3518139 [23] and the datasets analyzed during
the current study at https://doi.org/10.5281/zenodo.3630205 [8]. We thank Dirk
Beyer for very useful feedback on an earlier version of the paper and assistance
with configuring nitwit for SV-COMP 2020.
5 We know whether these programs are (non-)terminating, as they were reviewed in
SV-COMP before including them in the competition on termination analysis.