Using Atoms to Simplify Distributed Programs Checking

The execution of a distributed program generates a large state space which needs to be checked in testing and debugging. This state space can be reduced by using atoms corresponding to code blocks before performing the checking of the required program properties. This paper presents our results in using atoms which are known at program design time for this purpose. We consider the impact of incomplete or incorrect knowledge of atoms on the validity of checking if a run is indeed atomic with respect to the identified atoms and if it satisfies the required program properties.