The patent badge is an abbreviated version of the USPTO patent document. The patent badge does contain a link to the full patent document.
The patent badge is an abbreviated version of the USPTO patent document. The patent badge covers the following: Patent number, Date patent was issued, Date patent was filed, Title of the patent, Applicant, Inventor, Assignee, Attorney firm, Primary examiner, Assistant examiner, CPCs, and Abstract. The patent badge does contain a link to the full patent document (in Adobe Acrobat format, aka pdf). To download or print any patent click here.
Patent No.:
Date of Patent:
Mar. 19, 2013
Filed:
Oct. 09, 2009
Thomas J. Ball, Mercer Island, WA (US);
Eleonora O. Bounimova, Redmond, WA (US);
Vladimir A. Levin, Redmond, WA (US);
Rahul Kumar, Redmond, WA (US);
Thomas J. Ball, Mercer Island, WA (US);
Eleonora O. Bounimova, Redmond, WA (US);
Vladimir A. Levin, Redmond, WA (US);
Rahul Kumar, Redmond, WA (US);
Microsoft Corporation, Redmond, WA (US);
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.