Patent ID: 8453116

Claim:
At a computer system in a computer networking environment including a plurality of computing systems, a computerized method of inferring invariants used to verify that a software program satisfies a program specification, the method comprising the following acts: identifying at a software code identification module a portion of a software program that is to be verified as meeting certain program specifications; determining at an invariant inferring module one or more invariants for the identified portion of the software program that is to be verified, the one or more invariants being determined by inferring them at least in part from the software program's semantics, and each inferred invariant comprising a linear inequality which is represented in two parts using first and second abstract domains, the first part being represented in the first abstract domain as a linear equality, and the second part being represented in the second abstract domain as an interval based on the linear equality for a selected variable; selecting at a variable selection module one or more variables that are applied to each linear inequality of an inferred invariant to form the linear equality and an interval based on the linear inequality for such inferred invariant; performing at an operation module a reduction operation on the selected one or more variables to tighten numerical bounds for the interval of the second part of the linear inequality of each inferred invariant; and performing at the operation module a join operation on the first and second parts of the linear inequality for each inferred invariant, the join operation producing precise abstraction of one or more possible software program states which indicate whether the identified portion of the software program that is to be verified meets program specifications.