Interpretation-Based Violation Witness Validation for C: NITWIT
43
For predicate ϕ over V , let v |= ϕ denote that ϕ holds in valuation v. A witness
automaton (WA) is a finite-state automaton (NFA) used by the validator to run
in parallel to the CFG such that a program run violating the specification is
accepted.
Definition 2 (Witness automaton). A witness automaton (WA)
A = (Q, Σ, δ, q 0 , q E ) for a CFG C = (L, l 0 , G, V ) is an NFA with states Q,
initial state q 0 ∈ Q and δ : Q × Σ → 2
Q as usual, q E the accepting state and
Σ ⊆ 2
G
× Φ, where Φ is the set of predicates over V .
The transitions of A have source code and guards [11] that identify program
edges and place constraints on variable assignments respectively. They correspond to pairs (D i , ϕ i ), where D i ⊆ G and ϕ i is a predicate over variables.
Definition 3 (Simulation). Let A = (Q, Σ, δ, q 0 , q E ) be a WA for a CFG
C = (L, l 0 , G, V ) and ρ = l 0
g1
− → . . .
gn
−→ l n a path in C. The run q 0
σ1
−→ . . .
σn
− − → q n
in A simulates ρ iff σ i+1 = (D i+1 , ϕ i+1 ) with (l i , g i+1 , l i+1 ) ∈ D i+1 and v i+1 |=
ϕ i+1 for some state (l i+1 , v i+1 ). The run is accepted if q n = q E and L(A) is the
set of words σ 1 . . . σ n for which A has an accepting run.
The path l 0
g1
− → . . .
gn
−→ l n represents a set of concrete program executions
(l 0 , v 0 ) → . . . (l n , v n ) in which variable x has value v i (x). The state conditions
ϕ i+1 restrict the set of concrete program executions to those for which v i+1 |=
ϕ i+1 , for all i < n. Thus, a predicate ϕ i+1 constrains the concrete values in C.
When a verifier checks a property, its output should not only be yes or no,
but preferably also a program execution that leads to the property violation.
It is not always easy to construct a precise program execution path, as various
verification techniques apply abstractions. This is taken into consideration in
the witness format, for they represent a part of the state space that contains a
property violation. The “narrower” the space they represent is, the easier it is
to re-verify that a property is truly violated. A trivial witness automaton, e.g.,
which consists of only an (accepting) state with a self-loop, does not restrict
the program’s execution at all. Witness validation essentially then requires a
verification from scratch. On the other hand, a precise witness permits only
program executions leading to an error state, thereby making the validation as
direct as possible.
Definition 4 (Exact Witness). Let A = (Q, Σ, δ, q 0 , q E ) be a WA for a CFG
C = (L, l 0 , G, V ) and L E ⊆ L be a set of error locations. A WA A is exact iff
for all (D 1 , ϕ 1 ) . . . (D n , ϕ n ) ∈ L(A) it holds for all path l 0
g1
− → . . .
gn
−→ l n of C:
if (l i , g i+1 , l i+1 ) ∈ D i+1 and v i+1 |= ϕ i+1 in state (l i+1 , v i+1 ) for all 0 ≤ i < n,
then l n ∈ L E .
3 Validators for Violation Witnesses
Apart from a new format for exchanging verification results, [11] also presents
a feasibility study with implementing both a witness producer and a validator in two well-established tools – CPAchecker and Ultimate Automizer.
43
For predicate ϕ over V , let v |= ϕ denote that ϕ holds in valuation v. A witness
automaton (WA) is a finite-state automaton (NFA) used by the validator to run
in parallel to the CFG such that a program run violating the specification is
accepted.
Definition 2 (Witness automaton). A witness automaton (WA)
A = (Q, Σ, δ, q 0 , q E ) for a CFG C = (L, l 0 , G, V ) is an NFA with states Q,
initial state q 0 ∈ Q and δ : Q × Σ → 2
Q as usual, q E the accepting state and
Σ ⊆ 2
G
× Φ, where Φ is the set of predicates over V .
The transitions of A have source code and guards [11] that identify program
edges and place constraints on variable assignments respectively. They correspond to pairs (D i , ϕ i ), where D i ⊆ G and ϕ i is a predicate over variables.
Definition 3 (Simulation). Let A = (Q, Σ, δ, q 0 , q E ) be a WA for a CFG
C = (L, l 0 , G, V ) and ρ = l 0
g1
− → . . .
gn
−→ l n a path in C. The run q 0
σ1
−→ . . .
σn
− − → q n
in A simulates ρ iff σ i+1 = (D i+1 , ϕ i+1 ) with (l i , g i+1 , l i+1 ) ∈ D i+1 and v i+1 |=
ϕ i+1 for some state (l i+1 , v i+1 ). The run is accepted if q n = q E and L(A) is the
set of words σ 1 . . . σ n for which A has an accepting run.
The path l 0
g1
− → . . .
gn
−→ l n represents a set of concrete program executions
(l 0 , v 0 ) → . . . (l n , v n ) in which variable x has value v i (x). The state conditions
ϕ i+1 restrict the set of concrete program executions to those for which v i+1 |=
ϕ i+1 , for all i < n. Thus, a predicate ϕ i+1 constrains the concrete values in C.
When a verifier checks a property, its output should not only be yes or no,
but preferably also a program execution that leads to the property violation.
It is not always easy to construct a precise program execution path, as various
verification techniques apply abstractions. This is taken into consideration in
the witness format, for they represent a part of the state space that contains a
property violation. The “narrower” the space they represent is, the easier it is
to re-verify that a property is truly violated. A trivial witness automaton, e.g.,
which consists of only an (accepting) state with a self-loop, does not restrict
the program’s execution at all. Witness validation essentially then requires a
verification from scratch. On the other hand, a precise witness permits only
program executions leading to an error state, thereby making the validation as
direct as possible.
Definition 4 (Exact Witness). Let A = (Q, Σ, δ, q 0 , q E ) be a WA for a CFG
C = (L, l 0 , G, V ) and L E ⊆ L be a set of error locations. A WA A is exact iff
for all (D 1 , ϕ 1 ) . . . (D n , ϕ n ) ∈ L(A) it holds for all path l 0
g1
− → . . .
gn
−→ l n of C:
if (l i , g i+1 , l i+1 ) ∈ D i+1 and v i+1 |= ϕ i+1 in state (l i+1 , v i+1 ) for all 0 ≤ i < n,
then l n ∈ L E .
3 Validators for Violation Witnesses
Apart from a new format for exchanging verification results, [11] also presents
a feasibility study with implementing both a witness producer and a validator in two well-established tools – CPAchecker and Ultimate Automizer.