Graphical Animations of State Machines. - Tam Thi Thanh Nguyen; Kazuhiro Ogata 001 (DASC/PiCom/DataCom/CyberSciTech, 2017)

A Way to Comprehend Counterexamples Generated by the Maude LTL Model Checker. - Tam Thi Thanh Nguyen; Kazuhiro Ogata 001 (SATE, 2017)

Graphically Perceiving Characteristics of the MCS Lock and Model Checking Them. - Tam Thi Thanh Nguyen; Kazuhiro Ogata 001 (SOFL+MSVL, 2017)

Guessing Properties of the Qlock Mutual Exclusion Protocol based on its Graphical Animations and confirming the Properties by Model Checking. - May Thu Aung; Tam Thi Thanh Nguyen; Kazuhiro Ogata 001 (ICSCA, 2018)

Analysis of Two Flawed Versions of A Mutual Exclusion Protocol with Maude and SMGA. - May Thu Aung; Tam Thi Thanh Nguyen; Kazuhiro Ogata 001 (ICSCA, 2018)