Verifying Array Manipulating Programs with
Full-Program Induction
Supratik Chakraborty
1 , Ashutosh Gupta
1 , and Divyesh Unadkat
1,2
1 Indian Institute of Technology Bombay, Mumbai, India
{supratik,akg}@cse.iitb.ac.in
2 TCS Research, Pune, India
divyesh.unadkat@tcs.com
Abstract. We present a full-program induction technique for proving (a
sub-class of) quantified as well as quantifier-free properties of programs
manipulating arrays of parametric size N . Instead of inducting over individual loops, our technique inducts over the entire program (possibly
containing multiple loops) directly via the program parameter N . Significantly, this does not require generation or use of loop-specific invariants.
We have developed a prototype tool Vajra to assess the efficacy of our
technique. We demonstrate the performance of Vajra vis-a-vis several
state-of-the-art tools on a set of array manipulating benchmarks.
1 Introduction
Programs with loops manipulating arrays are common in a variety of applications. Unfortunately, assertion checking in such programs is undecidable. Existing tools therefore use a combination of techniques that work well for certain
classes of programs and assertions, and yield conservative results otherwise. In
this paper, we present a new technique to add to this arsenal of techniques.
Specifically, we focus on programs with loops manipulating arrays, where the
size of each array is a symbolic integer parameter N (> 0). We allow (a subclass of) quantified and quantifier-free pre- and post-conditions that may depend
on the symbolic parameter N . Thus, the problem we wish to solve can be viewed
as checking the validity of a parameterized Hoare triple {ϕ(N )} P N {ψ(N )} for
all values of N (> 0), where the program P N computes with arrays of size N ,
and N is a free variable in ϕ(·) and ψ(·). Fig. 1(a) shows an example of one such
Hoare triple, written using assume and assert. This triple effectively verifies
that
i−1
j=0
1 +
j−1
k=0 6 · (k + 1)
= i
3 for all i ∈ {0 . . . N −1}, and for all N > 0.
Although each loop in Fig. 1(a) is simple, their sequential composition makes it
difficult even for state-of-the-art tools like VIAP [26], VeriAbs [8], FreqHorn
[10], Tiler [4], Vaphor [24], or Booster [1] to prove the post-condition correct. In
fact, none of the above tools succeed in automatically proving the post-condition
in Fig. 1(a). In contrast, the technique presented in this paper, called full-program
induction, proves the post-condition in Fig. 1(a) correct within a few seconds.
Like several earlier approaches [29], full-program induction relies on mathematical induction to reason about programs with loops. However, the way in
c
The Author(s) 2020
A. Biere and D. Parker (Eds.): TACAS 2020, LNCS 12078, pp. 22–39, 2020.
https://doi.org/10.1007/978-3-030-45190-5 2
TACAS
Evaluation
Artifact
2020
Accepted
Full-Program Induction
Supratik Chakraborty
1 , Ashutosh Gupta
1 , and Divyesh Unadkat
1,2
1 Indian Institute of Technology Bombay, Mumbai, India
{supratik,akg}@cse.iitb.ac.in
2 TCS Research, Pune, India
divyesh.unadkat@tcs.com
Abstract. We present a full-program induction technique for proving (a
sub-class of) quantified as well as quantifier-free properties of programs
manipulating arrays of parametric size N . Instead of inducting over individual loops, our technique inducts over the entire program (possibly
containing multiple loops) directly via the program parameter N . Significantly, this does not require generation or use of loop-specific invariants.
We have developed a prototype tool Vajra to assess the efficacy of our
technique. We demonstrate the performance of Vajra vis-a-vis several
state-of-the-art tools on a set of array manipulating benchmarks.
1 Introduction
Programs with loops manipulating arrays are common in a variety of applications. Unfortunately, assertion checking in such programs is undecidable. Existing tools therefore use a combination of techniques that work well for certain
classes of programs and assertions, and yield conservative results otherwise. In
this paper, we present a new technique to add to this arsenal of techniques.
Specifically, we focus on programs with loops manipulating arrays, where the
size of each array is a symbolic integer parameter N (> 0). We allow (a subclass of) quantified and quantifier-free pre- and post-conditions that may depend
on the symbolic parameter N . Thus, the problem we wish to solve can be viewed
as checking the validity of a parameterized Hoare triple {ϕ(N )} P N {ψ(N )} for
all values of N (> 0), where the program P N computes with arrays of size N ,
and N is a free variable in ϕ(·) and ψ(·). Fig. 1(a) shows an example of one such
Hoare triple, written using assume and assert. This triple effectively verifies
that
i−1
j=0
1 +
j−1
k=0 6 · (k + 1)
= i
3 for all i ∈ {0 . . . N −1}, and for all N > 0.
Although each loop in Fig. 1(a) is simple, their sequential composition makes it
difficult even for state-of-the-art tools like VIAP [26], VeriAbs [8], FreqHorn
[10], Tiler [4], Vaphor [24], or Booster [1] to prove the post-condition correct. In
fact, none of the above tools succeed in automatically proving the post-condition
in Fig. 1(a). In contrast, the technique presented in this paper, called full-program
induction, proves the post-condition in Fig. 1(a) correct within a few seconds.
Like several earlier approaches [29], full-program induction relies on mathematical induction to reason about programs with loops. However, the way in
c
The Author(s) 2020
A. Biere and D. Parker (Eds.): TACAS 2020, LNCS 12078, pp. 22–39, 2020.
https://doi.org/10.1007/978-3-030-45190-5 2
TACAS
Evaluation
Artifact
2020
Accepted