Parallel State-Space Exploration in an Infinite-State Model Checker

Sammanfattning

This thesis presents the parallelization of the Counterexample-Guided Abstraction Refinement(CEGAR) algorithm in the Eldarica model checker. Eldarica, developed at Uppsala University, isa tool used for verifying systems modeled by Horn clauses, Numerical Transition Systems, andsoftware programs. The primary aim of this project was to identify parallelizable components within Eldarica'sCEGAR loop, design a parallel algorithm for the abstract reachability graph computation, andimplement it using Scala's Futures for concurrent execution. The parallel version demonstratedcorrect results and solved more benchmarks than the base version. Speed-up was observed inparticular for benchmarks with longer running time, indicating improved performance. The report discusses the design choices, implementation details, evaluation results andpotential future enhancements.