Nowadays, the complexity of systems continues to grow to the point where it is often impossible to analyse them in their entirety. Many of these systems govern our daily lives, from financial management to transportation, including the industries that surround us. A problem in one of these systems can have repercussions on the safety and lives of users.

In an effort to combat these errors, software modelling and verification have become increasingly popular over the decades. Modelling focusses on representing the problem we want to solve, while verification involves checking that the model behaves as expected. In reality, the task of verification is so complex that it becomes impossible to carry out.

To reduce the underlying complexity of model sizes, the symbolic approach is generally used. In our thesis, we developed an original symbolic method. This solution is based on the notion of encoding with internal operations, called homomorphisms. Just as integer intervals encode sets of integers and benefit from operations that work directly on these intervals instead of the sets, our new approach replicates this principle on intervals of vectors. These vectors encode the states of the systems to be verified.

Our new method has enabled the verification of properties on models that are still too complex even for the best tools, using the results of the Model Checking Contest 2022.