Partial Order Reduction for PINS

There are a lot of different tools used for formal verification of hard- and software. Both for the scientific purpose of comparing methods and tools, as well as the industrial use cases which may require combining various methods, a uniform interface for state space generation would improve the applicability of model checkers. One such interface is the partitioned next state interface (PINS) [5] which is an abstraction layer between the model and the algorithms used for state space generation. In this thesis we develop a partial order algorithm that works using a minimal extension of the PINS interface, and is developed in a modular fashion.