Modular variable abstraction for compositional verification with CEGAR

There are countless critical infrastructure operated by PLC at CERN. To mitigate the huge risk associated with the failure of these systems, it is desired to properly verify the software running on them. Model checking is a powerful tool to extend the verification workflow, and it is already used at CERN to verify the most critical programs. For large industrial processes, a framework called UNICOS is used to standardize and simplify the development. The code - and subsequently the model - generated by such frameworks is too large and complex to be effectively verified by model checking. This report provides a potential solution to this big challenge by combining two existing approaches.