Patent Document ID: 20120151449
Application ID: 13314738
Patent Flag: 0

Claim One:
1. A computer implemented method for the adaptive, scope bounded verification of computer software programs comprising the steps of: a) performing an automated pattern-based specification inference on the whole computer software program to compute likely function pre-conditions and function post-conditions; b) generating multiple analysis instances from the whole computer software program by selecting functions to be treated as entry points for the analysis; c) choosing a scope bound vector for the instance using previous results stored in an analysis results records database; d) performing an analysis for the bounded instance; e) storing analysis results in the analysis results records database; and f) periodically performing the above steps a-e; wherein the scope bound vector is adaptively chosen non-monotonically after each iteration and wherein the analysis is performed such that the computed likely function pre-conditions and function post-conditions are weaved into the analysis instance at the function scope boundary.