42
J. ˇ
Svejda et al.
properties as above. It does so for C programs. In contrast to most other validators (a) it does not rely on an existing software model checker, and (b) exploits
an interpretation-based approach. nitwit uses a home-made extension of the
PicoC interpreter which feeds a witness automaton with steering information
during a step-by-step interpretation of the C program, see Figure 1. nitwit was
evaluated on 11 533 violation witnesses in the ReachSafety category during SVCOMP 2020 and we compared its outcomes to another five witness validators
that participated. nitwit was able to validate more witnesses in this category
(8 526 in total) than all its competitors, and did so substantially faster. In addition, nitwit was able to validate 399 witnesses that could not be validated with
any of the five competitors.
Witness Automaton
Interpreter
C code
GraphML
false
unknown
NITWIT
replies,
resolves non-determinism
drives and provides
control flow + variables
VERIFIER error()
terminate
Fig. 1: High-level architecture of the nitwit Validator.
2 Background
The need for achieving portability of counterexamples and proofs between tools
gave rise to a type of non-deterministic finite automaton (NFA) called a witness
automaton, or simply a witness [11]. Two types of witnesses exist – a violation
and a correctness witness. In this paper, we focus on violation witnesses.
The concepts defined in this section follow the definitions of [22,11]. We
represent programs by control-flow graphs (CFGs).
Definition 1 (Control-flow graph). A control-flow graph C = (L, l 0 , G, V ) is
a finite set of locations L, initial location l 0 ∈ L, G ⊆ L × Op ×L a set of edges
where Op = {skip, assume(ϕ), assign(x, E)} with x ∈ V, ϕ a predicate over the
program variables V and E an expression over V .
In a CFG over V = {x, y}, e.g., an assignment is of the form x := x + y. The
interpretation of a CFG is given by a (possibly countably infinite) transition
system where states are of the form (l, v) where l ∈ L and v is a variable
assignment over V . For the sake of brevity, we refrain from a formal definition.
J. ˇ
Svejda et al.
properties as above. It does so for C programs. In contrast to most other validators (a) it does not rely on an existing software model checker, and (b) exploits
an interpretation-based approach. nitwit uses a home-made extension of the
PicoC interpreter which feeds a witness automaton with steering information
during a step-by-step interpretation of the C program, see Figure 1. nitwit was
evaluated on 11 533 violation witnesses in the ReachSafety category during SVCOMP 2020 and we compared its outcomes to another five witness validators
that participated. nitwit was able to validate more witnesses in this category
(8 526 in total) than all its competitors, and did so substantially faster. In addition, nitwit was able to validate 399 witnesses that could not be validated with
any of the five competitors.
Witness Automaton
Interpreter
C code
GraphML
false
unknown
NITWIT
replies,
resolves non-determinism
drives and provides
control flow + variables
VERIFIER error()
terminate
Fig. 1: High-level architecture of the nitwit Validator.
2 Background
The need for achieving portability of counterexamples and proofs between tools
gave rise to a type of non-deterministic finite automaton (NFA) called a witness
automaton, or simply a witness [11]. Two types of witnesses exist – a violation
and a correctness witness. In this paper, we focus on violation witnesses.
The concepts defined in this section follow the definitions of [22,11]. We
represent programs by control-flow graphs (CFGs).
Definition 1 (Control-flow graph). A control-flow graph C = (L, l 0 , G, V ) is
a finite set of locations L, initial location l 0 ∈ L, G ⊆ L × Op ×L a set of edges
where Op = {skip, assume(ϕ), assign(x, E)} with x ∈ V, ϕ a predicate over the
program variables V and E an expression over V .
In a CFG over V = {x, y}, e.g., an assignment is of the form x := x + y. The
interpretation of a CFG is given by a (possibly countably infinite) transition
system where states are of the form (l, v) where l ∈ L and v is a variable
assignment over V . For the sake of brevity, we refrain from a formal definition.