54
J. ˇ
Svejda et al.
nondeterminism, there exists only a single path through the program. If this
leads to an error location, then the validator may confidently claim that the
provided program and witness constitute a specification violation.
nitwit guarantees (except for implementation bugs, supported syntax and
available stack- and heap size) a validated violation witness iff it allows only such
abstract paths that end in an error location. Thus, given a well-specified exact
witness, nitwit should always find a violation, because it has the program state
space restricted to only such paths which reach an error location. If a witness
allows inexact abstract paths, then nitwit (and in fact also an execution-based
validator) may select the wrong path and see no error state. Results in Section 5
demonstrate that even without the guarantee of exact witnesses, interpretationbased validators can find a substantial amount of violations.
Finding violations. Results clearly show that nitwit is a competitive validator of
witnesses for C programs and invariant properties. Our validators implemented
independently of any verification platform can efficiently reestablish violations
from witnesses. We outperform other tools especially on the less time intensive
instances as nitwit works well in validating witnesses that restrict the state
space sufficiently. For these witnesses, it is the fastest among state-of-the-art
validators and has the smallest memory footprint.
We attribute the good outcomes in speed and memory to the choice of employing an interpretation-based approach. As nitwit explores only one path, it
is obviously faster than full fledged model-checking validators that explore many
paths. Interestingly, an interpreter-based execution analysis is often much faster
than compiled. This difference might be attributed to the fact that executionbased tools build the whole AST and CFG, whereas PicoC saves a lot of time
by not having to construct them. Moreover, a compiler translates the program
into machine code, a non-trivial task which PicoC circumvents.
Weaknesses. One of nitwit’s limitations is inherent to exploring only a single execution. Suppose a non-terminating program P , a trivial witness without
assumptions and a property violation, whose reachability depends on a nondeterministic variable being zero. nitwit, if it cannot resolve a nondeterministic
variable, assumes it has value one. In such a setting, the simulated program
diverges and so does nitwit, because it cannot recognize an infinite execution.
A similar situation may occur even if the witness is non-trivial. If its transitions
are not matched to the right operations (which can be a fault in both the witness
producer or validator), then P will diverge due to unresolved nondeterminism.
Secondly, as we employ an interpreter, there is a noticeable overhead compared to compiled programs in terms of CPU instructions per operation. Therefore, even if an execution is finite or reaches a violation in finitely many steps,
it might simply be too computationally intensive for nitwit to provide an answer within time. Combined with unresolved nondeterminism, this explained a
relatively high amount of Timeout results in an early version of nitwit benchmarked on SV-COMP 2019.
To combat the timeouts, we decided to implement a simple check in the witness automaton. After a certain number of unsuccessful transitions to a different
J. ˇ
Svejda et al.
nondeterminism, there exists only a single path through the program. If this
leads to an error location, then the validator may confidently claim that the
provided program and witness constitute a specification violation.
nitwit guarantees (except for implementation bugs, supported syntax and
available stack- and heap size) a validated violation witness iff it allows only such
abstract paths that end in an error location. Thus, given a well-specified exact
witness, nitwit should always find a violation, because it has the program state
space restricted to only such paths which reach an error location. If a witness
allows inexact abstract paths, then nitwit (and in fact also an execution-based
validator) may select the wrong path and see no error state. Results in Section 5
demonstrate that even without the guarantee of exact witnesses, interpretationbased validators can find a substantial amount of violations.
Finding violations. Results clearly show that nitwit is a competitive validator of
witnesses for C programs and invariant properties. Our validators implemented
independently of any verification platform can efficiently reestablish violations
from witnesses. We outperform other tools especially on the less time intensive
instances as nitwit works well in validating witnesses that restrict the state
space sufficiently. For these witnesses, it is the fastest among state-of-the-art
validators and has the smallest memory footprint.
We attribute the good outcomes in speed and memory to the choice of employing an interpretation-based approach. As nitwit explores only one path, it
is obviously faster than full fledged model-checking validators that explore many
paths. Interestingly, an interpreter-based execution analysis is often much faster
than compiled. This difference might be attributed to the fact that executionbased tools build the whole AST and CFG, whereas PicoC saves a lot of time
by not having to construct them. Moreover, a compiler translates the program
into machine code, a non-trivial task which PicoC circumvents.
Weaknesses. One of nitwit’s limitations is inherent to exploring only a single execution. Suppose a non-terminating program P , a trivial witness without
assumptions and a property violation, whose reachability depends on a nondeterministic variable being zero. nitwit, if it cannot resolve a nondeterministic
variable, assumes it has value one. In such a setting, the simulated program
diverges and so does nitwit, because it cannot recognize an infinite execution.
A similar situation may occur even if the witness is non-trivial. If its transitions
are not matched to the right operations (which can be a fault in both the witness
producer or validator), then P will diverge due to unresolved nondeterminism.
Secondly, as we employ an interpreter, there is a noticeable overhead compared to compiled programs in terms of CPU instructions per operation. Therefore, even if an execution is finite or reaches a violation in finitely many steps,
it might simply be too computationally intensive for nitwit to provide an answer within time. Combined with unresolved nondeterminism, this explained a
relatively high amount of Timeout results in an early version of nitwit benchmarked on SV-COMP 2019.
To combat the timeouts, we decided to implement a simple check in the witness automaton. After a certain number of unsuccessful transitions to a different