Verifying array manipulating programs by tiling

DOI10.1007/978-3-319-66706-5_21zbMATH Open1420.68066arXiv1707.03555OpenAlexW3101568729MaRDI QIDQ5233256FDOQ5233256

Authors: Supratik Chakraborty, Ashutosh Gupta, Divyesh Unadkat 

Publication date: 16 September 2019

Published in: Static Analysis (Search for Journal in Brave)

Abstract: Formally verifying properties of programs that manipulate arrays in loops is computationally challenging. In this paper, we focus on a useful class of such programs, and present a novel property-driven verification method that first infers array access patterns in loops using simple heuristics, and then uses this information to compositionally prove universally quantified assertions about arrays. Specifically, we identify tiles of array accesses patterns in a loop, and use the tiling information to reduce the problem of checking a quantified assertion at the end of a loop to an inductive argument that checks only a slice of the assertion for a single iteration of the loop body. We show that this method can be extended to programs with sequentially composed loops and nested loops as well. We have implemented our method in a tool called Tiler. Initial experiments show that Tiler outperforms several state-of-the-art tools on a suite of interesting benchmarks.

Full work available at URL: https://arxiv.org/abs/1707.03555

Recommendations

• Verifying array manipulating programs with full-program induction
• Automatic Verification of Integer Array Programs
• Property checking array programs using loop shrinking
• A rule-based verification strategy for array manipulating programs
• Verifying Array Programs by Transforming Verification Conditions

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Cited In (6)

• Verifying array manipulating programs with full-program induction
• Property checking array programs using loop shrinking
• Automatic Verification of Integer Array Programs
• \textsc{Diffy}: inductive reasoning of array programs using difference invariants
• Verifying Array Programs by Transforming Verification Conditions
• Booster: an acceleration-based verification framework for array programs

This page was built for publication: Verifying array manipulating programs by tiling

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5233256)