Verifying array manipulating programs by tiling

DOI10.1007/978-3-319-66706-5_21MaRDI QIDQ5233256zbMATH OpenOpenAlexFDO

Authors Supratik Chakraborty, Ashutosh Gupta, Divyesh Unadkat

Publication date 16 September 2019

Published in Static Analysis (Search for Journal in Brave)

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

Mathematics Subject Classification ID

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

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.

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

Cited in

(6)

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

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)