Verifying Array Manipulating Programs by Tiling

Project Description

In this project, we have developed a novel property-driven verification method that can infer array access patterns in loops, and use this information to compositionally prove universally quantified assertions about arrays. We have implemented our method in a tool called TILER which outperforms several state-of-the-art tools on a suite of interesting benchmarks.

Resources

• SAS 2017 conference paper is downloadable from Springer and arXiv.

• Code and benchmarks for the TILER tool from this paper can be found here.

• An extended set of slides on this work are available here.

• This work was featured at Winter School in Software Engineering 2017. The sildes can be viewed here.

• This work was also featured at the 2nd Indian SAT+SMT School 2017.

• TILER 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 downloadable from Springer.