Interpretation-Based Violation Witness
Validation for C: NITWIT
Jan ˇ
Svejda , Philipp Berger , and Joost-Pieter Katoen
RWTH Aachen University, Germany
{berger, katoen}@cs.rwth-aachen.de
jan.svejda@rwth-aachen.de
Abstract. As software verification is gaining traction in academia and
industry the number and complexity of verification tools is growing constantly. This initiated research and interest into exchangeable verification witnesses as well as tools for automated witness validation. Initial
witness validators used model checkers that were amended to benefit
from guidance information provided by the witness. This approach comes
with substantial overhead. Second-generation execution-based validators
traded speed for reduced strength in case of incomplete and non-exact
witnesses. This was done by extracting test harnesses and compiling
them with the original program. We present the nitwit tool, a new
interpretation-based violation witness validator for C programs that is
trimmed to be fast and memory efficient. It verifies a record number
of witnesses of SV-COMP’20 in the ReachSafety category. Our novel
tool exchanges initial compilation overhead and optimized execution for
rapid startup performance. nitwit borrows C semantics from the compiler used for compilation. This offloads this hard-to-get-right task and
enables using several compilers in parallel to inspect possible semantic
differences.
1 Introduction
The importance of witnesses. Model checking is a very successful automated verification technique with many applications. Its usage is rapidly increasing and
one may fairly argue that model checking has penetrated various industries. This
is true as well for software model checkers that, as opposed to first generation
model checkers, directly verify program code. Model checking is in particular a
very effective bug hunting technique: in case a property is violated, a counterexample is provided witnessing the property’s violation. This is why they are often
named witnesses. As phrased by Clarke et al. [16] “It is impossible to overestimate the importance of the counterexample feature. The counterexamples are
invaluable in debugging complex systems. Some people use model checking just
for this feature.”
Witness validation. Early model checkers provided witnesses for safety properties such as “certain bad states should always be avoided” as finite paths that
c
The Author(s) 2020
A. Biere and D. Parker (Eds.): TACAS 2020, LNCS 12078, pp. 40–57, 2020.
https://doi.org/10.1007/978-3-030-45190-5 3
TACAS
Evaluation
Artifact
2020
Accepted
Validation for C: NITWIT
Jan ˇ
Svejda , Philipp Berger , and Joost-Pieter Katoen
RWTH Aachen University, Germany
{berger, katoen}@cs.rwth-aachen.de
jan.svejda@rwth-aachen.de
Abstract. As software verification is gaining traction in academia and
industry the number and complexity of verification tools is growing constantly. This initiated research and interest into exchangeable verification witnesses as well as tools for automated witness validation. Initial
witness validators used model checkers that were amended to benefit
from guidance information provided by the witness. This approach comes
with substantial overhead. Second-generation execution-based validators
traded speed for reduced strength in case of incomplete and non-exact
witnesses. This was done by extracting test harnesses and compiling
them with the original program. We present the nitwit tool, a new
interpretation-based violation witness validator for C programs that is
trimmed to be fast and memory efficient. It verifies a record number
of witnesses of SV-COMP’20 in the ReachSafety category. Our novel
tool exchanges initial compilation overhead and optimized execution for
rapid startup performance. nitwit borrows C semantics from the compiler used for compilation. This offloads this hard-to-get-right task and
enables using several compilers in parallel to inspect possible semantic
differences.
1 Introduction
The importance of witnesses. Model checking is a very successful automated verification technique with many applications. Its usage is rapidly increasing and
one may fairly argue that model checking has penetrated various industries. This
is true as well for software model checkers that, as opposed to first generation
model checkers, directly verify program code. Model checking is in particular a
very effective bug hunting technique: in case a property is violated, a counterexample is provided witnessing the property’s violation. This is why they are often
named witnesses. As phrased by Clarke et al. [16] “It is impossible to overestimate the importance of the counterexample feature. The counterexamples are
invaluable in debugging complex systems. Some people use model checking just
for this feature.”
Witness validation. Early model checkers provided witnesses for safety properties such as “certain bad states should always be avoided” as finite paths that
c
The Author(s) 2020
A. Biere and D. Parker (Eds.): TACAS 2020, LNCS 12078, pp. 40–57, 2020.
https://doi.org/10.1007/978-3-030-45190-5 3
TACAS
Evaluation
Artifact
2020
Accepted