Scaling Formal Verification: Parallel Analysis of Functions

Formal methods have been known to be useful for verifying critical software. However, one of the main factors keeping tools such as CPA-Checker from being more widely adopted in industry is the prohibitive amount of time it takes to verify complex programs. We wish to address this by making CPAChecker scalable via divide-and-conquer and parallelization. We want to come up with a mechanical approach for decomposing verification tasks into subtasks that can verified individually. As soon as one subtask finds a violation, we abort the rest and return the violation.