Verifying Array Manipulating Programs with Full-Program Induction

Project Description

Formally verifying properties of programs that manipulate arrays of parametric size, in loops is computationally challenging. In this project, we have developed the Full-Program Induction technique for proving (a sub-class of) quantified as well as quantifier-free assertions in such programs. In this technique, we induct over the entire program via the program parameter N. We have demonstrated the effectiveness of our tool VAJRA vis-a-vis several verification tools on a set of array manipulating benchmarks. VAJRA is integrated into VeriAbs, a verification tool from TCS, which has won several accolades at the International Software Verification Competition.

Resources

• This work is invited to the International Journal on Software Tools for Technology Transfer STTT. It can be downloaded from here.

• TACAS 2020 conference paper is open-access and downloadable from Springer and arXiv.

• TACAS 2020 Artifact can be found on figshare and GitHub.

• TACAS 2020 conference presentation (online from morressier) can be accessed here.

• VAJRA is integrated with the verification tool called VeriAbs since year 2020. VeriAbs participates in SV-COMP and won a Gold medal in the ReachSafety category in SV-COMP 2020 where VAJRA and TILER helped VeriAbs perform better on Arrays Sub-category as compared to previous years. A paper describing this integration is freely downloadable from Springer.

• A set of slides on this work are available here.

• An online presentation on this work was presented at the 5th Indian SAT+SMT School 2020 is available on YouTube.

• An online presentation of this work was presented at SERI 2020 is available on YouTube.

• A poster on this work was presented at the 4th Indian SAT+SMT School 2019 can be seen here.