Mec 5 and AltaRica

In this presentation, we will present the Mec 5 verification tool and its environment. In particular, we will talk about the AltaRica formalism which has been developed in Bordeaux for more than ten years. We will then focus on two aspects of Mec 5: - its technical basis, mainly BDDs. We will try to show what we learned from our experimentations with BDDs in the last years - its very powerful logic which allows to express for example bisimilarity between two models, and we will show here how to use this logic to compute the winning strategies in parity games.