Software is an integral part of control mechanisms across industry ranging from avionics to medical. With 
the rights of technologies such as IoT, there is a great need to ensure that software is error free. 
However, each year there are hundreds of recorded software failures impacting billions of people and 
business losses in several billion dollars. Areas are extensively used to model software. Components such 
as batteries, sensors and so on in such software. Proving properties of programs with arrays is important 
but challenging. Our collaborative work with IT Bombay, addresses this challenge by targeting a class of 
business and safety critical applications across industries and can automatically prove correctness and 
safety properties in real time. Our novel technique called full program induction, proves properties of 
programs with potentially unbounded arrays. We perform induction on the symbolic size of arrays given as a 
program parameter. Performing the inductive step is particularly challenging. We have come up with the 
notion of difference program and difference property. That capitalized on the synergies between 
mathematical induction and difference computation, enabling the inductive step of the analysis. We use 
compiler frameworks such as LLVM for program transformations and SMT solvers such as Z3 for proving the 
validity of formulas newer techniques. Are continuously trying to push the boundary in this field, and our 
world is at the forefront improving properties of programs with arrays. We have implemented the algorithms 
for full program induction in a verification tool called Vajra. Is now integrated with the TCS 
Verification Framework Query Apps that has won several gold medals at the International Software 
Verification Competition. On a longer term, our technique will find applications across industries to 
avoid monetary losses, loss of credibility and unforeseen project delays by early detection of errors and 
proving their absence.