Today, some software programs contain one million lines of code (LOC) or more. In order to ensure the reliability of these software programs, the software programs undergo testing before releasing the software programs to consumers. A first phase of testing is commonly referred to as verification testing. Verification testing attempts to find errors in the source code of the program. The identified errors may then be corrected before the software program undergoes another phase of testing, commonly referred to as run-time, or beta testing.
One approach for performing verification testing of software programs is based on dataflow analysis. In dataflow analysis, a property that is being tested is analyzed through each path of the program. The analysis determines a state for the property at each point in the program and maintains information regarding the state of the property. Upon traversing two paths of a branch statement, the analysis may determine that the property could be in multiple states at the end of the branch statement. These multiple states are combined and carried forward in the analysis. Later, when another branch statement occurs, the analysis traverses both paths of the branch statement using the combined multiple states. This method of analysis is extremely efficient. However, the results are not very accurate. Typically, the results indicate an error in the source code even when the source code does not have errors. A programmer is then responsible for reviewing the source code and for determining which reported errors are actual errors. Even though dataflow analysis provides inaccurate results, it is commonly performed on both small and large software programs.
Another approach for performing verification testing of software programs is commonly referred to as path-sensitive analysis. Briefly, path-sensitive analysis tracks a concrete state of the program (e.g., values of variables). Therefore, when a branch statement occurs in the program, path-sensitive analysis uses the concrete state to determine which paths of the branch statement are feasible. The feasible paths are then traversed. Whenever the analysis cannot determine which path of the branch statement to traverse based on the concrete state, the analysis duplicates the concrete state so that both paths may modify their copy of the concrete state as needed. This duplication of the concrete state at each branch statement greatly increases the search space and is commonly referred to as “search space explosion”. For example, if a program has one hundred (100) branches, the search space may grow exponentially by 2100. This exponential growth of the search space limits path-sensitive analysis to small software programs.
Until the present invention, full-scale reliable verification of a software program having a large code base was unattainable.