Formal verification of Anderson mutual exclusion protocol by introducing an auxiliary variable (S). - Naoki Asae; Duong Dinh Tran; Kazuhiro Ogata 001 (SEKE, 2021)