Evaluating compositional verification options for PLCverif

Model checking is a computationally complex task and state space explosion often hinders successful verification. Compositional (also called modular) verification techniques aim to tackle this by decomposing model checking problems into smaller sub-problems that are potentially easier to compute, and reasoning about the original problem through them. The main focus of my summer student project was evaluating the state of the art in compositional verification and examining how they could be applied in PLCverif, a model checking framework for PLC programs developed at CERN.