Verifying Array Manipulating Programs with Full-Program Induction
37
Name #L T1
T2
T3 T4
T5
T6
pcomp 3 0.68 TO TO ?0.23 TO ?0.58
ncomp 3 0.68 TO TO ?0.41 TO ?0.68
eqnm2 2 0.52 TO TO ?0.07 TO ?0.59
eqnm3 2 0.53 TO TO ?0.07 TO ?0.56
eqnm4 2 0.51 TO TO ?0.07 TO ?0.60
eqnm5 2 0.55 TO TO ?0.07 TO ?0.58
sqm
2 0.51 69.7 TO ?0.11 TO ?0.57
res1
4 0.17 TO TO TO
TO
TO
res1o
4 0.18 TO TO TO
TO
TO
res2
6 0.20 TO TO TO
TO
TO
res2o
6 0.22 TO TO TO
TO
TO
ss1
4 0.40 TO TO 0.13 ?19.2 ?1.7
ss2
6 0.46 TO TO 0.13 TO ?9.7
ss3
5 0.35 TO TO 0.13 TO ?2.1
ss4
4 0.29 TO TO 0.13 TO ?1.6
ssina
5 0.41 72.5 TO TO
TO ?2.0
sina1
2 0.56 65.4 TO TO
TO
TO
sina2
3 0.69 66.5 TO TO
TO
TO
sina3
4 0.83 TO TO TO
TO
TO
sina4
4 0.85 TO TO TO
TO
TO
sina5
5 0.93 TO TO TO
TO
TO
Name
#L T1
T2
T3
T4
T5
T6
zerosum1
2 0.33 62.0 11 0.77 0.29 TO
zerosum2
4 0.46 75.8 18
TO
1.64 TO
zerosum3
6 0.59 73.1 39
TO
3.13 TO
zerosum4
8 0.76 76.1 TO ?18.2 6.85 TO
zerosum5 10 0.97 80.6 TO ?16.5 10.4 TO
zerosumm2 4 0.46 71.5 24
TO
1.22 TO
zerosumm3 6 0.59 70.9 TO
TO
5.22 TO
zerosumm4 8 0.77 76.4 TO ?16.7 12.39 TO
zerosumm5 10 0.98 81.7 TO ?18.7 22.8 TO
zerosumm6 12 1.29 86.8 TO ?16.1 TO
TO
copy9
9 0.69 86.8 3.91 18.8 TO 0.67
min
1 0.48 23.6 3.82 0.52 0.14 0.13
max
1 0.46 25.4 4.70 1.0 0.28 0.18
compare
1 0.82 18.8 17.9 0.06 0.84 0.31
conda
3 0.72 13.9 TO 0.07 0.09 TO
condn
1 ?0.51 14.7 18.9 0.02 0.15 0.20
condm
2 ?0.59 20.5 16.7 0.04 TO
-
condg
3 ?0.52 TO
TO
TO
TO
TO
modn
2 ?0.63 22.6 TO
-
TO
TO
mods
4 ?0.61 TO 18.2
-
-
-
modp
2 ?0.71 17.3 40
-
?32
-
Table 1. First column is the benchmark name. Second column indicates the number
loops in the benchmark (excluding the assertion loop). Successive columns indicate the
results generated by tools and the time taken where T1 is Vajra, T2 is VIAP, T3
is VeriAbs, T4 is Booster, T5 is Vaphor, T6 is FreqHorn. indicates assertion
safety, indicates assertion violation, ? indicates unknown result, and - indicates an
abrupt stop. All the times are in seconds. TO is time-out of 100 secs.
to prove the assertions. VeriAbs reported 1 program as unsafe due to the imprecision of its abstractions and it proved 4 benchmarks that Vajra could not.
Vajra verified 30 benchmarks that Booster could not. Booster reported 4
benchmarks as unsafe due to imprecise abstractions, its fixed-point computation
engine reported unknown result on 12 benchmarks and it ended abruptly on
3 benchmarks. Booster also proved 2 benchmarks that couldn’t be handled
by the current version of Vajra due to syntactic limitations. Vajra verified
32 benchmarks on which Vaphor was inconclusive. Distinguished cell abstraction in Vaphor is unable to prove safety of programs, when the value at each
array index needs to be tracked. Vaphor reported 9 programs unsafe due to
imprecise abstraction, returned unknown on 2 programs and ended abruptly on
1 program. Vaphor proved a benchmark that Vajra could not. Vajra verified 32 programs on which FreqHorn diverged, especially when constants and
terms that appear in the inductive invariant are not syntactically present in the
program. FreqHorn ran out of time on 22 programs, reported unknown result
on 12 and ended abruptly on 3 benchmarks. FreqHorn verified a benchmark
with a single loop that Vajra could not. On an extended set of 231 benchmarks,
Vajra verified 110 programs out of 121 safe programs, falsified 108 out of 110
unsafe programs, and was inconclusive on the remaining 13 programs.
5 Conclusion
We presented a novel property-driven verification method that performs induction over the entire program via parameter N . Significantly, this obviates the
need for loop-specific invariants. Experiments show that full-program induction
performs remarkably well vis-a-vis state-of-the-art tools for analyzing array manipulating programs. Further improvements in the algorithms for computing difference programs and for strengthening of pre- and post-conditions are envisaged
as part of future work.
37
Name #L T1
T2
T3 T4
T5
T6
pcomp 3 0.68 TO TO ?0.23 TO ?0.58
ncomp 3 0.68 TO TO ?0.41 TO ?0.68
eqnm2 2 0.52 TO TO ?0.07 TO ?0.59
eqnm3 2 0.53 TO TO ?0.07 TO ?0.56
eqnm4 2 0.51 TO TO ?0.07 TO ?0.60
eqnm5 2 0.55 TO TO ?0.07 TO ?0.58
sqm
2 0.51 69.7 TO ?0.11 TO ?0.57
res1
4 0.17 TO TO TO
TO
TO
res1o
4 0.18 TO TO TO
TO
TO
res2
6 0.20 TO TO TO
TO
TO
res2o
6 0.22 TO TO TO
TO
TO
ss1
4 0.40 TO TO 0.13 ?19.2 ?1.7
ss2
6 0.46 TO TO 0.13 TO ?9.7
ss3
5 0.35 TO TO 0.13 TO ?2.1
ss4
4 0.29 TO TO 0.13 TO ?1.6
ssina
5 0.41 72.5 TO TO
TO ?2.0
sina1
2 0.56 65.4 TO TO
TO
TO
sina2
3 0.69 66.5 TO TO
TO
TO
sina3
4 0.83 TO TO TO
TO
TO
sina4
4 0.85 TO TO TO
TO
TO
sina5
5 0.93 TO TO TO
TO
TO
Name
#L T1
T2
T3
T4
T5
T6
zerosum1
2 0.33 62.0 11 0.77 0.29 TO
zerosum2
4 0.46 75.8 18
TO
1.64 TO
zerosum3
6 0.59 73.1 39
TO
3.13 TO
zerosum4
8 0.76 76.1 TO ?18.2 6.85 TO
zerosum5 10 0.97 80.6 TO ?16.5 10.4 TO
zerosumm2 4 0.46 71.5 24
TO
1.22 TO
zerosumm3 6 0.59 70.9 TO
TO
5.22 TO
zerosumm4 8 0.77 76.4 TO ?16.7 12.39 TO
zerosumm5 10 0.98 81.7 TO ?18.7 22.8 TO
zerosumm6 12 1.29 86.8 TO ?16.1 TO
TO
copy9
9 0.69 86.8 3.91 18.8 TO 0.67
min
1 0.48 23.6 3.82 0.52 0.14 0.13
max
1 0.46 25.4 4.70 1.0 0.28 0.18
compare
1 0.82 18.8 17.9 0.06 0.84 0.31
conda
3 0.72 13.9 TO 0.07 0.09 TO
condn
1 ?0.51 14.7 18.9 0.02 0.15 0.20
condm
2 ?0.59 20.5 16.7 0.04 TO
-
condg
3 ?0.52 TO
TO
TO
TO
TO
modn
2 ?0.63 22.6 TO
-
TO
TO
mods
4 ?0.61 TO 18.2
-
-
-
modp
2 ?0.71 17.3 40
-
?32
-
Table 1. First column is the benchmark name. Second column indicates the number
loops in the benchmark (excluding the assertion loop). Successive columns indicate the
results generated by tools and the time taken where T1 is Vajra, T2 is VIAP, T3
is VeriAbs, T4 is Booster, T5 is Vaphor, T6 is FreqHorn. indicates assertion
safety, indicates assertion violation, ? indicates unknown result, and - indicates an
abrupt stop. All the times are in seconds. TO is time-out of 100 secs.
to prove the assertions. VeriAbs reported 1 program as unsafe due to the imprecision of its abstractions and it proved 4 benchmarks that Vajra could not.
Vajra verified 30 benchmarks that Booster could not. Booster reported 4
benchmarks as unsafe due to imprecise abstractions, its fixed-point computation
engine reported unknown result on 12 benchmarks and it ended abruptly on
3 benchmarks. Booster also proved 2 benchmarks that couldn’t be handled
by the current version of Vajra due to syntactic limitations. Vajra verified
32 benchmarks on which Vaphor was inconclusive. Distinguished cell abstraction in Vaphor is unable to prove safety of programs, when the value at each
array index needs to be tracked. Vaphor reported 9 programs unsafe due to
imprecise abstraction, returned unknown on 2 programs and ended abruptly on
1 program. Vaphor proved a benchmark that Vajra could not. Vajra verified 32 programs on which FreqHorn diverged, especially when constants and
terms that appear in the inductive invariant are not syntactically present in the
program. FreqHorn ran out of time on 22 programs, reported unknown result
on 12 and ended abruptly on 3 benchmarks. FreqHorn verified a benchmark
with a single loop that Vajra could not. On an extended set of 231 benchmarks,
Vajra verified 110 programs out of 121 safe programs, falsified 108 out of 110
unsafe programs, and was inconclusive on the remaining 13 programs.
5 Conclusion
We presented a novel property-driven verification method that performs induction over the entire program via parameter N . Significantly, this obviates the
need for loop-specific invariants. Experiments show that full-program induction
performs remarkably well vis-a-vis state-of-the-art tools for analyzing array manipulating programs. Further improvements in the algorithms for computing difference programs and for strengthening of pre- and post-conditions are envisaged
as part of future work.