Farn Wang
Real-world softwares for concurrent systems may involve data-structures linked together with pointers. Even with such sophistication, they are usually supposed to work regardless of the number of processes. We propose a new automatic approximation method to safely verify algorithms used in such systems. The central idea is to construct a finite collective image set (CIS) which collapses reachable state representations for all implementations of all numbers of processes. Our collapsing scheme filters out unimportant information of system behaviors and results in CIS's with manageable space requirements which allow for efficient verification. Analysis shows our method can automatically generate a CIS of size 657 to verify that a version of Mellor-Crummy & Scott's algorithm preserves mutual exclusion for all numbers of processes.