1. A computer-implemented method of verifying a software program, said method comprising the computer implemented steps of: performing a transformation of the software program source code by adding assertions that permit the detection of violations of verification properties; generating a model which defines a set of executions of the transformed source code; analyzing the model to verify the software program; generating error traces when property violations are discovered; and outputting the error traces indicative of the property violations; THE METHOD CHARCTERIZED IN THAT: a range analysis is performed thereby generating a bounded range of values for one or more variables in the transformed source code wherein prior to the range analysis the variables may take the full range of integer values; the generated bounded ranges of values are used by the analyzing step thereby reducing the size of the variables in the model such that the sizes of the reduced variables are still large enough to represent all possible values during execution of the program; creating three variables v.sub.p, v′.sub.p, v″.sub.p with a declaration of int**p, said v.sub.p standing for p, v′.sub.p for *p, and v″.sub.p for **p, and wherein variables representing pointers are desugared into variables of type unsigned int; performing a first assignment to one of the three variables; and performing a two conditional assignment based on the first assignment and aliasing of the variables.