Browse Prior Art Database

Scalable Analysis via Expanding Scopes

IP.com Disclosure Number: IPCOM000247378D
Publication Date: 2016-Aug-30
Document File: 1 page(s) / 24K

Publishing Venue

The IP.com Prior Art Database

Abstract

Disclosed is a staged expanding-scope method for interprocedural abstract interpretation, which invokes sound analysis with partial programs of increasing scope.

This text was extracted from a PDF file.
This is the abbreviated version, containing approximately 74% of the total text.

Page 01 of 1

Scalable Analysis via Expanding Scopes

A system or method is needed to enable scalable inter-procedural analysis.

The novel contribution is a staged expanding-scopemethod for interprocedural abstract interpretation, which invokes sound analysis with partial programs of increasing scope. This method achieves many benefits typical of whole-program interprocedural analysis, but scales to large programs by limiting analysis to small program fragments. To address cases in which the static analysis of program fragments fails to prove safety, the analysis also suggests possible annotations, which, if a user accepts, ensure the desired properties.

The disclosed staged analysis adapts the cost of the analysis to the difficulty of the verification task. The analysis breaks the verification problem into multiple sub-problems and adapts the analysis of each sub-problem along two dimensions: the

precision dimension and the analysis-scope dimension. The analysis adapts the

precision (and thus the expected cost) of the abstract interpretation to the difficulty of verifying the sub-problem. The novelty of this approach is the ability to adapt the scope of the analyzed program fragment to the difficulty of the verification task. Unlike existing staged techniques, which analyze whole programs, this new analysis operates on program fragments .

The basic idea is to break the program into fragments and separately analyze each fragment, making conservative assumptions about the part...