Towards scalable software analysis using combinations and conditions with CPACHECKER

Verification of large-scale programs is a challenging problem. Software analysis tools focus on making a verification task both precise and efficient. We implemented the software analysis tool CPAchecker based on the configurable program analysis framework. CPAchecker aims to make it possible for a user to integrate and configure an analysis technique to the tool easily. In order to handle large-scale programs, software analysis techniques use abstraction which introduce unsoundness and incompleteness to the process. If the sources of unsoundness and incompleteness is defined and evaluated by the user, the analysis will still be useful for finding potential bugs in the program. In our work, we used two related mechanisms to define and control potential sources of imprecision: Verification assumptions and verification conditions. Assumptions can be represented as a state predicate (a logical formula) that specify under what assumption an abstract state was reached during the analysis. Verification conditions are used as commands to guide the tool when some specific behaviour is observed during the analysis. In this thesis, we use verification assumptions and conditions to guide the analysis process. We added functionalities to CPAchecker such that it provides three mechanisms: (i) Starting the analysis task with a set of specified assumptions to run a partial verification. (ii) Using conditional analysis to increase the coverage of analysis and generating an analysis report encoded as assumptions even in cases where the conventional model checking fails to handle. (iii) Restarting the analysis with a set of different conditions and assumptions or deploying another analysis technique using an analysis report that has been already generated. We extended CPAchecker to include a sequential composition framework that restarts the analysis with a new configuration using the result of another analysis. In our implementation of CPAchecker, the process of assumption and verification condition generation is automated. Experimental results have shown us that using the configurable program analysis concept and guiding the analysis using assumptions and verification conditions was able to find bugs that traditional techniques were not able to identify, and increase the efficiency and precision of the analysis.