Verification of array manipulating programs
2
MINS READ
Leading the way in innovation for over 50 years, we build greater futures for businesses across multiple industries and 131 countries.
Our expert, committed team put our shared beliefs into action – every day. Together, we combine innovation and collective knowledge to create the extraordinary.
We share news, insights, analysis and research – tailored to your unique interests – to help you deepen your knowledge and impact.
At TCS, we believe exceptional work begins with hiring, celebrating and nurturing the best people — from all walks of life.
Get access to a catalog of the latest news stories from across TCS. Discover our press releases, reports, and company announcements.
Divyesh Unadkat, Scientist, TCS Research
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.
Ecosystem Modeling in a Digitally Simulated Electricity Market
Empowering Forest Landowners to Measure and Monetize Carbon Credits
A Journey from Software Development to Visual Intelligence Research
A robust architecture for real-time satellite sensing data