US 2011/0088016 A1 · PROGRAM ANALYSIS THROUGH PREDICATE ABSTRACTION AND REFINEMENT

Abstract

An analysis engine is described for performing static analysis using CEGAR loop functionality, using a combination of forward and backward validation-phase trace analyses. The analysis engine includes a number of features. For example: (1) the analysis engine can operate on blocks of program statements of different adjustable sizes; (2) the analysis engine can identify a subtrace of the trace and perform analysis on that subtrace (rather than the full trace); (3) the analysis engine can form a pyramid of state conditions and extract predicates based on the pyramid and/or from auxiliary source(s); (4) the analysis engine can generate predicates using an increasingly-aggressive series of available discovery techniques; (5) the analysis engine can selectively concretize procedure calls associated with the trace on an as-needed basis and perform other refinements; and (6) the analysis engine can add additional verification targets in the course of its analysis, etc.

Claims20

Dependent claims

A method, implemented by a computer device, for validating a candidate trace produced by a Counter-Example Guided Abstraction Refinement (CEGAR) loop, the candidate trace associated with a potential error within a program, the method comprising:

performing forward analysis in a forward direction along the candidate trace to collect information pertaining to the candidate trace;
performing backward analysis in a backward direction along the candidate trace, on the basis of the information collected in the forward analysis,
the forward analysis and the backward analysis identifying whether the candidate trace represents a feasible trace or an infeasible trace;
and
generating, for the case of an infeasible trace, at least one predicate for use in removing the infeasible trace from a subsequent iteration of the CEGAR loop if said at least one predicate can be discovered.

2 more elements

An analysis engine, implemented by a computer device, for performing static analysis, comprising:

an abstract IR generating (AIR-generating) module for receiving an instrumented intermediate representation (IR) program associated with an input program, and based thereon, producing an abstract IR (AIR) program, the AIR program including plural blocks, at least one of the blocks including plural statements of the IR program;
a Boolean program-generating module for generating a Boolean program based on the AIR program and a current set of predicates, the Boolean program-generating module transforming blocks of the AIR program into a Boolean form using respective transformers;
a model checking module for identifying a candidate trace using the Boolean program, the candidate trace associated with a potential error in the AIR program;
and
a validation module for determining whether the candidate trace represents a feasible trace or an infeasible trace, and if the candidate trace is an infeasible trace, for generating at least one predicate for use in removing the infeasible trace from subsequent analysis of the AIR program, if said at least one predicate can be discovered,
the validation module comprising:
a forward analysis module for operating in a forward direction along the candidate trace to collect information pertaining to the candidate trace;
and
a backward analysis module for operating in a backward direction along the candidate trace, on the basis of the information collected in the forward analysis.

6 more elements

Dependencies are inferred from the claim text.

Program analysis through predicate abstraction and refinement

Life of this patent

Program analysis through predicate abstraction and refinement

Life of this patent

Abstract

Claims20