A scalable, computer implemented method for finding subtle flaws in software programs. The method advantageously employs 1) scope bounding which limits the size of a generated model by excluding deeply-nested function calls, where the scope bounding vector is chosen non-monotonically, and 2) automatic specification inference which generates constraints for functions through the effect of a light-weight and scalable global analysis. Advantageously, scalable software model checking is achieved while at the same time finding more bugs.