44
J. ˇ
Svejda et al.
Subsequently, [12] reports on two more validators that extract test harnesses
from violation witnesses to perform validation. A test harness is compiled with
the program to supply input values during runtime and provide definitions
for necessary external functions. This approach differs from tools using formal
verification/model-checking techniques by offloading semantics to a compiler and
only investigating a single path through the program. Validators that explore a
single path through compilation/execution are called execution-based validators.
In addition, a new validator MetaVal
1 was introduced in SV-COMP 2020 – we
refrain from describing it as it is yet to be published though we do include it in
the benchmark evaluation. All five validators participated in SV-COMP.
CPAchecker This tool employs a so-called Configurable Program Analysis
(CPA), which allows selecting the desired level of precision to control the tradeoff between performance gain and spurious counterexamples [13]. When witness validation is enabled, it matches a witness automaton against the program’s CFG. Afterwards, as part of the CPA, it strengthens the exploration
with state-space guards from the witness at matched locations. [11] reports that
e.g. their value analysis and predicate analysis are capable of using this strengthening [15,14].
Ultimate Automizer This tool uses an automata-based approach to verification [19,18,17]. Prior to the analysis, it transforms programs into a variant of
CFGs over an alphabet of program statements. Such a CFG, say C error , recognizes control-flow traces – sequences of statements – that lead to a property
violation. A control-flow trace is feasible if it is a run of C error and ends in
an accepting error state. For validation, the tool creates a new CFG C w from
the Cartesian product of the C error and a witness automaton. Subsequently, the
tool runs the same analysis over the CFG C w as for a usual verification run
and validates the witness if an error trace is found. State-space guards, such as
ϕ i+1 in Definition 3 over control edges and source code guards that characterize
branching are ignored.
CPA-witness2test This tool exploits the verifier of CPAchecker. It constructs and matches a CFG with the witness, but does not perform a CPA analysis. It collects the input and initialization values from matched assumptions and
assembles an ordered vector of values for every used nondeterministic function,
which it then transforms into a switch statement supplied as function implementation. For uninitialized variables, which in C are also nondeterministic, no
values are injected.
In automatic software verification, programs are usually decorated with an
external function VERIFIER error to identify a point which should never be
reached, i.e., an error location. CPA-witness2test implements the function
as a call to exit(107), which immediately terminates an execution with return
1 https://gitlab.com/sosy-lab/software/metaval
J. ˇ
Svejda et al.
Subsequently, [12] reports on two more validators that extract test harnesses
from violation witnesses to perform validation. A test harness is compiled with
the program to supply input values during runtime and provide definitions
for necessary external functions. This approach differs from tools using formal
verification/model-checking techniques by offloading semantics to a compiler and
only investigating a single path through the program. Validators that explore a
single path through compilation/execution are called execution-based validators.
In addition, a new validator MetaVal
1 was introduced in SV-COMP 2020 – we
refrain from describing it as it is yet to be published though we do include it in
the benchmark evaluation. All five validators participated in SV-COMP.
CPAchecker This tool employs a so-called Configurable Program Analysis
(CPA), which allows selecting the desired level of precision to control the tradeoff between performance gain and spurious counterexamples [13]. When witness validation is enabled, it matches a witness automaton against the program’s CFG. Afterwards, as part of the CPA, it strengthens the exploration
with state-space guards from the witness at matched locations. [11] reports that
e.g. their value analysis and predicate analysis are capable of using this strengthening [15,14].
Ultimate Automizer This tool uses an automata-based approach to verification [19,18,17]. Prior to the analysis, it transforms programs into a variant of
CFGs over an alphabet of program statements. Such a CFG, say C error , recognizes control-flow traces – sequences of statements – that lead to a property
violation. A control-flow trace is feasible if it is a run of C error and ends in
an accepting error state. For validation, the tool creates a new CFG C w from
the Cartesian product of the C error and a witness automaton. Subsequently, the
tool runs the same analysis over the CFG C w as for a usual verification run
and validates the witness if an error trace is found. State-space guards, such as
ϕ i+1 in Definition 3 over control edges and source code guards that characterize
branching are ignored.
CPA-witness2test This tool exploits the verifier of CPAchecker. It constructs and matches a CFG with the witness, but does not perform a CPA analysis. It collects the input and initialization values from matched assumptions and
assembles an ordered vector of values for every used nondeterministic function,
which it then transforms into a switch statement supplied as function implementation. For uninitialized variables, which in C are also nondeterministic, no
values are injected.
In automatic software verification, programs are usually decorated with an
external function VERIFIER error to identify a point which should never be
reached, i.e., an error location. CPA-witness2test implements the function
as a call to exit(107), which immediately terminates an execution with return
1 https://gitlab.com/sosy-lab/software/metaval