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:
Sep. 15, 2009
Filed:
Apr. 15, 2005
Bor-yuh Evan Chang, Berkeley, CA (US);
K. Rustan Leino, Bellevue, WA (US);
Bor-Yuh Evan Chang, Berkeley, CA (US);
K. Rustan Leino, Bellevue, WA (US);
Microsoft Corporation, Redmond, WA (US);
Abstract
A local analysis analyzes the values of objects paying attention to program flow and a global analysis analyses the object independent of the flow. The local and global analysis interact to infer the invariants of objects used within a computer program. The local analysis is given the known invariants of an object by the global analysis when the object transitions from a valid to a mutable state. It then keeps track of all of the values of objects encountered until the object transitions from mutable to a valid state, when the information known to the local analysis is passed to the global analysis, which may use the new object values to add to the current list of invariants for the given object.