Adjustable Block Analysis: Actor-based Creation of Block Summaries for Scaling Formal Verification

Software quality assurance becomes more and more popular in modern software development. Fixing bugs early, reduces the cost and increases the quality of the product. Since a great portion of time is needed for debugging, assisting techniques are integrated. Many techniques use formal verification as a basis. Although formal verification is applied with great success to many software development pipelines, the scalability is still a big challenge. In this work, we introduce the concept of the distributed CPAs (configurable program analyses). The core idea is to partition the control flow automaton (CFA) of a given input program in coherent blocks with one entry and one exit node. Workers analyze every block parallely and broadcast new information to every other worker. If a block contains an error location, the block is analyzed backwards from the error location. Whenever the analysis reaches the top of the block, we ask whether other blocks can prove the error location (un)reachable. For this, we can reuse the results of previous verification runs on other blocks. Our approach is easily extensible to support any existing configurable program analysis and additionally allows an easy integration of other concepts, e.g., fault localization. This work shows and explains the implementation of a framework for distributed CPAs in CPAchecker. Furthermore, we perform a thorough evaluation of the approach, showing that our implementation is sound and matches the results of the existing predicate analysis. However, the great amount of transferred data between workers slows down the verification process causing many out-of-memory errors and timeouts. Nonetheless, the evaluation reveals the current bottle-necks and points us to potentially useful and effective improvements.

Thesis: https://www.sosy-lab.org/research/msc/2022.Kettl.Adjustable_Block_Analysis.pdf