Enhancing Distributed Summary Synthesis with Data-Flow Analysis

With increasing software complexity, scalable and precise verification is essential, especially in safety-critical areas. Distributed Summary Synthesis (DSS) supports scalability by enabling parallel processing of program segments (blocks). However, it faces limitations in achieving early-stage abstraction due to the inherent laziness of Predicate Analysis, which only refines abstractions when errors are detected. This thesis addresses this by integrating Data-Flow Analysis (DFA) into DSS, enhancing the initial information shared among program blocks to potentially accelerate and improve verification. Implemented in CPAchecker, DFA runs in parallel with Predicate Analysis, providing coarse summaries that strengthen the preconditions for successor blocks. Experimental evaluation using SV-COMP 2024 benchmarks, however, indicated that while DFA integration occasionally improved verification coverage, it also introduced additional resource demands. This increase in CPU time, wall time and memory usage, due to message handling and serialization and deserialization overhead, limited the number of programs that could be verified compared to the DSS implementation with only predicate analysis. This trade-off suggests that additional optimizations are needed to reduce performance costs and better harness the potential of DFA for scalable and effective verification.