Skip to main content
Skip to footer

Author

Divyesh Unadkat, Scientist, TCS Research

 

Highlights

  • A novel technique called 'Full-Program Induction' uses mathematical induction to prove precision of parametric programs.
  • Instead of inducting individual loops, the technique inducts the entire program, directly via a program parameter.
  • A prototype tool, Vajra, is developed to assess the efficacy of the technique.

My paper in 2 minutes

Verification of array manipulating programs

 

 

Automatically proving that the software used in day-to-day devices will function correctly is challenging. In this paper, that was presented at the International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) 2020, we designed a novel technique called 'Full-Program Induction' that uses mathematical induction to prove correctness of parametric programs. 

Instead of inducting over individual loops, it inducts the entire program, possibly containing multiple loops, directly via a program parameter, say N. The induction technique automatically computes the ‘difference’ between programs with different values of the symbolic parameter, N. This difference is used to prove the inductive step of the analysis. 

The technique focuses on proving a sub-class of quantified as well as quantifier-free properties of parametric programs that manipulate arrays.  While automatically generating loop-specific quantified invariants is difficult, our technique does not require such invariants to prove the correctness of programs with arrays. A prototype tool, Vajra, has been developed to assess the efficacy of Full-Program Induction. The performance of Vajra vis-a-vis several state-of-the-art tools is demonstrated on a set of arrays manipulating benchmarks from verification competitions and industrial code repositories.