36
S. Chakraborty et al.
While we have presented our technique focusing on a single symbolic parameter N , a straightforward extension works for multiple independent parameters,
multiple independent array sizes, different induction directions, and non-uniform
loop termination conditions. For more details, please refer to the long version of
our paper at [3].
Limitations. There are several scenarios under which full-program induction
may not produce a conclusive result. Currently, we only analyze programs with
non-nested loops with +, −, ×, ÷ expressions in assignments. We also do not
handle branch conditions that are dependent on the parameter N (this doesn’t
include loop conditions, which are handled by unrolling the loop). The technique
also remains inconclusive when the difference program ∂P N does not have fewer
loops than the original program. Reduction in verification complexity of the program, in terms of the number of loops and assignment statements dependent on
N , is crucial to the success of full-program induction. Finally, our technique may
fail to verify a correct program if the heuristics used for weakest pre-condition
either fail or return a pre-condition that causes violation of the base case check
in line 18 of FPIVerify. Despite these limitations, our experiments show that
full-program induction performs remarkably well on a large suite of benchmarks.
4 Implementation and Experiments
We have implemented our technique in a prototype tool called Vajra, available
at [5]. It takes a C program in SVCOMP format as input. The tool, written
in C++, is built on top of the LLVM/CLANG [22] 6.0.0 compiler infrastructure
and uses Z3 [25] v4.8.7 as the SMT solver to prove Hoare triples for loop-free
programs.
We have evaluated Vajra on a test-suite of 42 safe benchmarks inspired from
different algebraic functions that compute polynomials as well as a standard
array operations such as copy, min, max and compare. Our programs take a
symbolic parameter N which specifies the size of each array as well as the number
of times each loop executes. Assertions, possibly quantified, are (in-)equalities
over array elements, scalars and (non-)linear polynomial terms over N .
All experiments were performed on a Ubuntu 18.04 machine with 16GB RAM
and running at 2.5 GHz. We have compared Vajra against VIAP(v1.0) [26], VeriAbs(v1.3.10) [8], Booster(v0.2) [1], Vaphor(v1.2) [24] and FreqHorn(v3)
[10]. C programs were manually converted to mini-Java as required by Vaphor
and CHC’s as required by FreqHorn. Our results are shown in Table 1. Vajra
verified 36 benchmarks, compared to 23 verified by VIAP, 12 by VeriAbs, 8 by
Booster, 5 each by Vaphor and FreqHorn. Vajra was unable to compute
the difference program for 5 benchmarks and was inconclusive on 1 benchmark.
Vajra verified 17 benchmarks on which VIAP diverged, primarily due to
the inability of VIAP’s heuristics to get closed form expressions. VIAP verified 4 benchmarks that could not be verified by the current version of Vajra due to syntactic limiations. Vajra, however, is two orders of magnitude
faster than VIAP on programs that were verified by both. Vajra proved 28
benchmarks on which VeriAbs diverged. VeriAbs ran out of time on programs where loop shrinking and merging abstractions were not strong enough
S. Chakraborty et al.
While we have presented our technique focusing on a single symbolic parameter N , a straightforward extension works for multiple independent parameters,
multiple independent array sizes, different induction directions, and non-uniform
loop termination conditions. For more details, please refer to the long version of
our paper at [3].
Limitations. There are several scenarios under which full-program induction
may not produce a conclusive result. Currently, we only analyze programs with
non-nested loops with +, −, ×, ÷ expressions in assignments. We also do not
handle branch conditions that are dependent on the parameter N (this doesn’t
include loop conditions, which are handled by unrolling the loop). The technique
also remains inconclusive when the difference program ∂P N does not have fewer
loops than the original program. Reduction in verification complexity of the program, in terms of the number of loops and assignment statements dependent on
N , is crucial to the success of full-program induction. Finally, our technique may
fail to verify a correct program if the heuristics used for weakest pre-condition
either fail or return a pre-condition that causes violation of the base case check
in line 18 of FPIVerify. Despite these limitations, our experiments show that
full-program induction performs remarkably well on a large suite of benchmarks.
4 Implementation and Experiments
We have implemented our technique in a prototype tool called Vajra, available
at [5]. It takes a C program in SVCOMP format as input. The tool, written
in C++, is built on top of the LLVM/CLANG [22] 6.0.0 compiler infrastructure
and uses Z3 [25] v4.8.7 as the SMT solver to prove Hoare triples for loop-free
programs.
We have evaluated Vajra on a test-suite of 42 safe benchmarks inspired from
different algebraic functions that compute polynomials as well as a standard
array operations such as copy, min, max and compare. Our programs take a
symbolic parameter N which specifies the size of each array as well as the number
of times each loop executes. Assertions, possibly quantified, are (in-)equalities
over array elements, scalars and (non-)linear polynomial terms over N .
All experiments were performed on a Ubuntu 18.04 machine with 16GB RAM
and running at 2.5 GHz. We have compared Vajra against VIAP(v1.0) [26], VeriAbs(v1.3.10) [8], Booster(v0.2) [1], Vaphor(v1.2) [24] and FreqHorn(v3)
[10]. C programs were manually converted to mini-Java as required by Vaphor
and CHC’s as required by FreqHorn. Our results are shown in Table 1. Vajra
verified 36 benchmarks, compared to 23 verified by VIAP, 12 by VeriAbs, 8 by
Booster, 5 each by Vaphor and FreqHorn. Vajra was unable to compute
the difference program for 5 benchmarks and was inconclusive on 1 benchmark.
Vajra verified 17 benchmarks on which VIAP diverged, primarily due to
the inability of VIAP’s heuristics to get closed form expressions. VIAP verified 4 benchmarks that could not be verified by the current version of Vajra due to syntactic limiations. Vajra, however, is two orders of magnitude
faster than VIAP on programs that were verified by both. Vajra proved 28
benchmarks on which VeriAbs diverged. VeriAbs ran out of time on programs where loop shrinking and merging abstractions were not strong enough