Skip to main content
Skip to footer
We're taking you to another TCS website now.

A full-program induction technique for proving quantified and quantifier-free properties of program manipulating arrays of parametric size N. A prototype tool Vajra is developed to assess the efficacy of the technique.

By Divyesh Unadkat, Supratik Chakraborty, Ashutosh Gupta

Error: unable to play the video

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.


Connect with us to transform your workplace

*Required field
*Enter valid First Name
First Name
*Required field
*Enter valid Last Name
Last Name
*Required field
*Email syntax error
*Please use your business email.
*Required field
*Enter valid company name
Company Name
What's your challenge

Thank you for your interest

We will shortly connect.

Click here to submit another form.