24
S. Chakraborty et al.
9-12). Unfortunately, automatically deriving such quantified non-linear loop invariants is far from trivial. Template-based invariant generators, viz. [12,9], are
among the best-performers when generating such complex invariants. However,
their abilities are fundamentally limited by the set of templates from which they
choose. We therefore choose not to depend on invariants for individual loops in
our work at all. Instead of inducting over the iterations of each individual loop,
we propose to reason about the entire program (containing one or more loops)
directly, while inducting on the parameter N . Needless to say, each approach
has its own strengths and limitations, and the right choice always depends on
the problem at hand. Our experiments show that full-program induction is able
to solve several difficult problem instances with an off-the-shelf SMT solver (Z3)
at the back-end, which other techniques either fail to solve these instances, or
rely on sophisticated recurrence solvers.
The primary contributions of our work can be summarized as follows.
– We introduce the notion of full-program induction for reasoning about assertions in programs with loops manipulating arrays.
– We present practical algorithms for full-program induction.
– We describe a prototype tool Vajra that implements the algorithms, using
an off-the-shelf SMT solver, viz. Z3, at the back-end to discharge verification
conditions. Vajra outperforms several state-of-the-art tools on a suite of
array-manipulating benchmark programs.
Related Work. Earlier work on inductive techniques can be broadly categorized
into those that require loop-specific invariants to be provided or automatically
generated, and those that work without them. Requiring a “good” inductive invariant for every loop in a program effectively shifts the onus of assertion checking
to that of invariant generation. Among techniques that do not require explicit
inductive invariants or mid-conditions for each loop, there are some that require
loop invariants to be implicitly generated by a constraint solver. These include
techniques based on constrained Horn clause solving [21,15,10,24], acceleration
and lazy interpolation for arrays [1] and those that use inductively defined predicates and recurrence solving [26,17], among others. Thanks to the impressive
capabilities of modern constraint solvers and the effectiveness of carefully tuned
heuristics for stringing together multiple solvers, this approach has shown a lot
of promise in recent years. However, at a fundamental level, these formulations
rely on solving implicitly specified loop invariants garbed as constraint solving
problems. There are yet other techniques, such as that in [28], that truly do
not depend on loop invariants being generated. In fact, the technique of [28]
comes closest to our work in principle. However, [28] imposes severe restrictions
on the input programs, and the example in Fig. 1 does not meet these restrictions. Therefore, the technique of [28] is applicable only to a small part of the
program-assertion space over which our technique works. Techniques such as
tiling [4] reason one loop at a time and apply only when loops have simple data
dependencies across iterations (called non-interference of tiles in [4]). It effectively uses a slice of the post-condition of a loop as an inductive invariant, and
S. Chakraborty et al.
9-12). Unfortunately, automatically deriving such quantified non-linear loop invariants is far from trivial. Template-based invariant generators, viz. [12,9], are
among the best-performers when generating such complex invariants. However,
their abilities are fundamentally limited by the set of templates from which they
choose. We therefore choose not to depend on invariants for individual loops in
our work at all. Instead of inducting over the iterations of each individual loop,
we propose to reason about the entire program (containing one or more loops)
directly, while inducting on the parameter N . Needless to say, each approach
has its own strengths and limitations, and the right choice always depends on
the problem at hand. Our experiments show that full-program induction is able
to solve several difficult problem instances with an off-the-shelf SMT solver (Z3)
at the back-end, which other techniques either fail to solve these instances, or
rely on sophisticated recurrence solvers.
The primary contributions of our work can be summarized as follows.
– We introduce the notion of full-program induction for reasoning about assertions in programs with loops manipulating arrays.
– We present practical algorithms for full-program induction.
– We describe a prototype tool Vajra that implements the algorithms, using
an off-the-shelf SMT solver, viz. Z3, at the back-end to discharge verification
conditions. Vajra outperforms several state-of-the-art tools on a suite of
array-manipulating benchmark programs.
Related Work. Earlier work on inductive techniques can be broadly categorized
into those that require loop-specific invariants to be provided or automatically
generated, and those that work without them. Requiring a “good” inductive invariant for every loop in a program effectively shifts the onus of assertion checking
to that of invariant generation. Among techniques that do not require explicit
inductive invariants or mid-conditions for each loop, there are some that require
loop invariants to be implicitly generated by a constraint solver. These include
techniques based on constrained Horn clause solving [21,15,10,24], acceleration
and lazy interpolation for arrays [1] and those that use inductively defined predicates and recurrence solving [26,17], among others. Thanks to the impressive
capabilities of modern constraint solvers and the effectiveness of carefully tuned
heuristics for stringing together multiple solvers, this approach has shown a lot
of promise in recent years. However, at a fundamental level, these formulations
rely on solving implicitly specified loop invariants garbed as constraint solving
problems. There are yet other techniques, such as that in [28], that truly do
not depend on loop invariants being generated. In fact, the technique of [28]
comes closest to our work in principle. However, [28] imposes severe restrictions
on the input programs, and the example in Fig. 1 does not meet these restrictions. Therefore, the technique of [28] is applicable only to a small part of the
program-assertion space over which our technique works. Techniques such as
tiling [4] reason one loop at a time and apply only when loops have simple data
dependencies across iterations (called non-interference of tiles in [4]). It effectively uses a slice of the post-condition of a loop as an inductive invariant, and