Interpretation-Based Violation Witness Validation for C: NITWIT
41
end in a bad state. A simple witness-steered simulation could reveal the flaw.
Modern model checkers heavily use abstraction, and witnesses are no longer concrete, but rather phrased in terms of some abstract model. This is in particular
true for software model checkers. Witnesses are in fact finite paths through an
abstracted program representing sets of paths in the concrete program that is to
be verified. These sets may contain spurious concrete paths. This raises the question whether witnesses are correct. Witness validation is the process of checking
whether a witness produced by a software model checker is indeed a witness
showing that the concrete program violates the property. Software model checkers such as CBMC, CPAchecker and so on, that generate witnesses are called
producers, while software tools that perform the witness validation are named
validators. With a single exception [12], existing validators are incorporated or
directly built on top of the existing software model checkers CPAchecker [13] or
Ultimate Automizer [19,18,17].
A format for witnesses. In order to facilitate the validation of witnesses by
various different tools, a witness format has been developed that nowadays is
used by many software model checkers. For safety properties as above, this format
prescribes how to represent a witness for reaching a bad state. Due to this
format, witnesses are exchangeable and witness validation can be done using
different techniques and tools. This format allows (i) a cross-platform exchange
of information that enables “drop-in” replacement of tools such as visualization
and reviews of results [10], (ii) validation of witnesses which strengthens trust in
verification results, especially if the verifier and validator use different techniques
and (iii) a significant amount of false bug alarms to be caught by failed validation.
Witness validation in software verification competitions. Since a few years, the
use of witnesses has become an important part in software competitions such as
the annual TACAS Competition on Software Verification (SV-COMP) [2,3,4,5,6].
SV-COMP is a competition in automatic software verification, in which academic, but also some industrial, software verifiers participate. In the 2019 edition [6], 31 verifiers participated in verifying 10 522 verification tasks for C programs (and 368 for Java programs). SV-COMP has different categories, such as
reachability, memory and concurrency safety, absence of overflows, and termination. SV-COMP adopted violation witnesses as part of its benchmark scoring
schema since 2015 [3] and adhered to it also in the following editions [4,5,6].
This means that a verifier does not receive a point for a violated property unless
the produced violation witness could be validated by at least one validator. This
applies to all categories. To reflect that violation witnesses contain sufficient information for validation, the validators are granted only limited resources (e.g.,
only 10% of the amount of time available for verification, and 7 GB memory).
Correctness witnesses were incorporated into the score evaluation in 2017 [5] –
since this competition, validated correctness witnesses yield a bonus point for
the producer.
Contributions of this paper. This paper presents the interpretation-based witness validator nitwit. It validates violation witnesses for safety reachability
41
end in a bad state. A simple witness-steered simulation could reveal the flaw.
Modern model checkers heavily use abstraction, and witnesses are no longer concrete, but rather phrased in terms of some abstract model. This is in particular
true for software model checkers. Witnesses are in fact finite paths through an
abstracted program representing sets of paths in the concrete program that is to
be verified. These sets may contain spurious concrete paths. This raises the question whether witnesses are correct. Witness validation is the process of checking
whether a witness produced by a software model checker is indeed a witness
showing that the concrete program violates the property. Software model checkers such as CBMC, CPAchecker and so on, that generate witnesses are called
producers, while software tools that perform the witness validation are named
validators. With a single exception [12], existing validators are incorporated or
directly built on top of the existing software model checkers CPAchecker [13] or
Ultimate Automizer [19,18,17].
A format for witnesses. In order to facilitate the validation of witnesses by
various different tools, a witness format has been developed that nowadays is
used by many software model checkers. For safety properties as above, this format
prescribes how to represent a witness for reaching a bad state. Due to this
format, witnesses are exchangeable and witness validation can be done using
different techniques and tools. This format allows (i) a cross-platform exchange
of information that enables “drop-in” replacement of tools such as visualization
and reviews of results [10], (ii) validation of witnesses which strengthens trust in
verification results, especially if the verifier and validator use different techniques
and (iii) a significant amount of false bug alarms to be caught by failed validation.
Witness validation in software verification competitions. Since a few years, the
use of witnesses has become an important part in software competitions such as
the annual TACAS Competition on Software Verification (SV-COMP) [2,3,4,5,6].
SV-COMP is a competition in automatic software verification, in which academic, but also some industrial, software verifiers participate. In the 2019 edition [6], 31 verifiers participated in verifying 10 522 verification tasks for C programs (and 368 for Java programs). SV-COMP has different categories, such as
reachability, memory and concurrency safety, absence of overflows, and termination. SV-COMP adopted violation witnesses as part of its benchmark scoring
schema since 2015 [3] and adhered to it also in the following editions [4,5,6].
This means that a verifier does not receive a point for a violated property unless
the produced violation witness could be validated by at least one validator. This
applies to all categories. To reflect that violation witnesses contain sufficient information for validation, the validators are granted only limited resources (e.g.,
only 10% of the amount of time available for verification, and 7 GB memory).
Correctness witnesses were incorporated into the score evaluation in 2017 [5] –
since this competition, validated correctness witnesses yield a bonus point for
the producer.
Contributions of this paper. This paper presents the interpretation-based witness validator nitwit. It validates violation witnesses for safety reachability