Formal Verification of Distributed Algorithms in +CAL 2.0

Master thesis, Master Informatique de NancyThere are some important challenges associated with distributed systems including race conditions and deadlocks. These systems thus should be verified before deployment. Algorithmic verification is a formal technique; it means that the verification is itself performed algorithmically, in contrast to manual or interactive verification. Algorithmic representation of a system can be achieved using +CAL developed by Leslie Lamport. This work aims at removing some of the limitations of the previous version of the +CAL language. We have validated our implementation by verifying some algorithms