Formal Verification of Concurrent Algorithms: Case Studies on Mutual Exclusion

Concurrent algorithms are difficult to design correctly. This study focused on mutual exclusion and explored the benefits of employing a formal approach for specifying and verifying concurrent algorithms through case studies. This paper reports the findings and insight obtained from the case studies, including the detection of a design fault in one of the analyzed algorithms.