Scope bounding with automated specification inference for scalable software model checking
View Patent ↗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.
1. A computer implemented method for adaptive, scope bounded verification of computer software programs comprising:
a) performing an automated pattern-based specification inference on a 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 an analysis;
c) choosing a scope bound vector for an instance using previous results stored in an analysis results records database;
d) performing the analysis for a 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.
2. The computer implemented method of claim 1 further comprising:
generating operator-initiated warnings from the results stored in the analysis results records database and initiating investigations.
3. The computer implemented method of claim 2 further comprising:
updating a source code repository with updated computer software program code such that a new analysis instance is generated.
4. The computer implemented method of claim 2 , further comprising:
modifying the function pre-conditions and post-conditions for the next iteration based on the analysis results and generated warnings.
5. The computer implemented method of claim 1 , wherein the pattern-based specification inference is based on syntactically matching expressions in the code and handling pointer indirections.
6. The computer implemented method of claim 1 , wherein the specification inference hoists annotations based on assertions inside a function to its start and across function calls.
7. The computer implemented method of claim 1 , wherein the specification inference hoists annotations based on potential runtime errors inside a function to its start and across function calls.
8. The computer implemented method of claim 7 , wherein the specification inference hoists annotations for potential runtime errors, including segmentation faults, buffer overflows, and memory leaks.