14
D. Beyer and M. Dangl
KI
←−DF: KI
←−DF [5] denotes a parallel combination of k -induction (without
property direction) with a data-flow-based auxiliary-invariant generator that
continuously supplies the k -induction procedure with invariants. Here, we
configure Alg. 1 such that pd = false and get_currently_known_invariant()
always returns the most recent (strongest) invariant computed by the dataflow-based auxiliary-invariant generator.
KI
←−KIPDR: Similarly to KI
←−DF, KI
←−KIPDR denotes a parallel combination of k -induction with an auxiliary-invariant generator — in this case,
KIPDR — that continuously supplies invariants to the k -induction procedure. Here, we configure one instance of Alg. 1 such that pd = false and
get_currently_known_invariant() always returns the most recent (strongest) invariant computed by KIPDR (a second instance of Alg. 1 that is configured such
that pd = true and get_currently_known_invariant() always returns true).
KI
←−DF;KIPDR KI
←−DF;KIPDR denotes a parallel combination of
k -induction with an auxiliary-invariant generator that uses a sequential combination of a data-flow-based invariant generator and KIPDR to continuously
supply k -induction with auxiliary invariants. We configure one instance of Alg. 1
such that pd = false and get_currently_known_invariant() always returns the
most recent (strongest) invariant computed by a sequential combination of
the data-flow-based invariant generator and KIPDR (a second instance of
Alg. 1 that runs after the invariant generator finishes and is configured such
that pd = true and get_currently_known_invariant() always returns true).
We do not evaluate the used invariant generators as standalone approaches, as
they are designed specifically to be used as auxiliary components and do not perform well enough in isolation. For example, data-flow based invariant-generation
approaches are often too imprecise to verify tasks, whereas more precise techniques
like KIPDR might run into too many timeouts to be competitive. Instead, we
use the framework of k -induction with continuously refined invariant generation,
which has been shown to be able to combine quick and precise techniques [5].
4.2 Experimental Setup
Details about the experimental setup can be found in the technical report [8],
which describes in Sect. 4.2 which tool versions and SMT theory we used, in
Sect. 4.3 which benchmark sets we used and why, in Sect. 4.4 which existing
verifiers we compared to and which versions we took, in Sect. 4.5 which computing
resources and execution environment were used, in Sect. 4.6 the scoring schema,
and in Sect. 4.12 which threats to the validity of the evaluation we identified
and how we mitigated them.
4.3 Results
In the following, we pick a few highlights from the results of our experimental evaluation, in order to illustrate the potential of the approaches. A complete and more
detailed report of the results is available in the extended version of this article [8].
D. Beyer and M. Dangl
KI
←−DF: KI
←−DF [5] denotes a parallel combination of k -induction (without
property direction) with a data-flow-based auxiliary-invariant generator that
continuously supplies the k -induction procedure with invariants. Here, we
configure Alg. 1 such that pd = false and get_currently_known_invariant()
always returns the most recent (strongest) invariant computed by the dataflow-based auxiliary-invariant generator.
KI
←−KIPDR: Similarly to KI
←−DF, KI
←−KIPDR denotes a parallel combination of k -induction with an auxiliary-invariant generator — in this case,
KIPDR — that continuously supplies invariants to the k -induction procedure. Here, we configure one instance of Alg. 1 such that pd = false and
get_currently_known_invariant() always returns the most recent (strongest) invariant computed by KIPDR (a second instance of Alg. 1 that is configured such
that pd = true and get_currently_known_invariant() always returns true).
KI
←−DF;KIPDR KI
←−DF;KIPDR denotes a parallel combination of
k -induction with an auxiliary-invariant generator that uses a sequential combination of a data-flow-based invariant generator and KIPDR to continuously
supply k -induction with auxiliary invariants. We configure one instance of Alg. 1
such that pd = false and get_currently_known_invariant() always returns the
most recent (strongest) invariant computed by a sequential combination of
the data-flow-based invariant generator and KIPDR (a second instance of
Alg. 1 that runs after the invariant generator finishes and is configured such
that pd = true and get_currently_known_invariant() always returns true).
We do not evaluate the used invariant generators as standalone approaches, as
they are designed specifically to be used as auxiliary components and do not perform well enough in isolation. For example, data-flow based invariant-generation
approaches are often too imprecise to verify tasks, whereas more precise techniques
like KIPDR might run into too many timeouts to be competitive. Instead, we
use the framework of k -induction with continuously refined invariant generation,
which has been shown to be able to combine quick and precise techniques [5].
4.2 Experimental Setup
Details about the experimental setup can be found in the technical report [8],
which describes in Sect. 4.2 which tool versions and SMT theory we used, in
Sect. 4.3 which benchmark sets we used and why, in Sect. 4.4 which existing
verifiers we compared to and which versions we took, in Sect. 4.5 which computing
resources and execution environment were used, in Sect. 4.6 the scoring schema,
and in Sect. 4.12 which threats to the validity of the evaluation we identified
and how we mitigated them.
4.3 Results
In the following, we pick a few highlights from the results of our experimental evaluation, in order to illustrate the potential of the approaches. A complete and more
detailed report of the results is available in the extended version of this article [8].