By Divyesh Unadkat, Supratik Chakraborty, Ashutosh Gupta
2021
Automatically proving that the software used in day-to-day devices will function correctly is challenging. In this paper, presented at the International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) 2020, we have 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.
