Permission inference for array programs

DOI10.1007/978-3-319-96142-2_7MaRDI QIDQ6039395zbMATH OpenOpenAlexFDO

Authors Jérôme Dohrau, Alexander J. Summers, C. Urban, Severin Münger, Peter Müller

Publication date 5 May 2023

Published in Computer Aided Verification (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70)

Abstract: Information about the memory locations accessed by a program is, for instance, required for program parallelisation and program verification. Existing inference techniques for this information provide only partial solutions for the important class of array-manipulating programs. In this paper, we present a static analysis that infers the memory footprint of an array program in terms of permission pre- and postconditions as used, for example, in separation logic. This formulation allows our analysis to handle concurrent programs and produces specifications that can be used by verification tools. Our analysis expresses the permissions required by a loop via maximum expressions over the individual loop iterations. These maximum expressions are then solved by a novel maximum elimination algorithm, in the spirit of quantifier elimination. Our approach is sound and is implemented; an evaluation on existing benchmarks for memory safety of array programs demonstrates accurate results, even for programs with complex access patterns and nested loops.

Recommendations

• Automatic inference of access permissions
• Array Abstractions from Proofs
• An Analysis of Permutations in Arrays
• Dependent array type inference from tests
• Non-disjunctive Numerical Domain for Array Predicate Abstraction

Cited in

(3)

• The map equality domain
• Access permission contracts for scripting languages
• Automatic inference of access permissions

This page was built for publication: Permission inference for array programs

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