Bugs in software and hardware can have a negative impact in many situations of our daily life and the severity of the impact can range from being simply annoying to being catastrophic and live-threatening. To avoid such mistakes there exist software tools for checking the correctness of soft- and hardware products. These tools receive as input the description of a soft- or hardware product, build an internal model for it, and then check certain properties of the model. The tools are, however, only able to find certain types of mistakes. Furthermore, as software and hardware products become more and more complex, the input for the verification tool is often huge so that it can take a very long time to execute and requires a large amount of space. In certain settings the tool can only partially check correctness and might not terminate at all.

In this project we developed new algorithms that are faster and use less storage space. Furthermore they are faster, not only in finding simple errors but also in finding more complex error than previous algorithms. We analyzed these algorithms theoretically and also implemented and evaluated them empirically. To design our algorithms we developed new algorithmic techniques as well as adapted techniques used previously for different kind of algorithms research. Furthermore we showed that our algorithmic approaches are applicable beyond verification, for example, in probabilistic planning and artificial intelligence.