Formal verification of mutual exclusion protocols

Using proof scores and CafeOBJ, we formally verify that (1) an abstract version of the Anderson mutual exclusion protocol (Tran & Ogata, 2020) and (2) an the MCS mutual exclusion protocol (Tran et al., 2020) enjoy the mutual exclusion property.

References

2020

SEKE

Formal verification of an abstract version of Anderson protocol with CafeOBJ, CiMPA and CiMPG

Duong Dinh Tran, and Kazuhiro Ogata

In The 32nd International Conference on Software Engineering and Knowledge Engineering, SEKE 2020, KSIR Virtual Conference Center, USA, July 9-19, 2020, 2020

DOI Bib

@inproceedings{DBLP:conf/seke/Tran020,
  author = {Tran, Duong Dinh and Ogata, Kazuhiro},
  editor = {Garc{\'{\i}}a{-}Castro, Ra{\'{u}}l},
  title = {Formal verification of an abstract version of Anderson protocol with
                    CafeOBJ, CiMPA and CiMPG},
  booktitle = {The 32nd International Conference on Software Engineering and Knowledge
                    Engineering, {SEKE} 2020, {KSIR} Virtual Conference Center, USA, July
                    9-19, 2020},
  pages = {287--292},
  publisher = {{KSI} Research Inc.},
  year = {2020},
  url = {https://doi.org/10.18293/SEKE2020-064},
  doi = {10.18293/SEKE2020-064},
  timestamp = {Sun, 12 Nov 2023 00:00:00 +0100},
  biburl = {https://dblp.org/rec/conf/seke/Tran020.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org},
}

APSEC

Lemma Weakening for State Machine Invariant Proofs

Duong Dinh Tran, Dang Duy Bui, Parth Gupta, and 1 more author

In 27th Asia-Pacific Software Engineering Conference, APSEC 2020, Singapore, December 1-4, 2020, 2020

DOI Bib

@inproceedings{DBLP:conf/apsec/TranBG020,
  author = {Tran, Duong Dinh and Bui, Dang Duy and Gupta, Parth and Ogata, Kazuhiro},
  title = {Lemma Weakening for State Machine Invariant Proofs},
  booktitle = {27th Asia-Pacific Software Engineering Conference, {APSEC} 2020, Singapore,
                    December 1-4, 2020},
  pages = {21--30},
  publisher = {{IEEE}},
  year = {2020},
  url = {https://doi.org/10.1109/APSEC51365.2020.00010},
  doi = {10.1109/APSEC51365.2020.00010},
  timestamp = {Sun, 12 Nov 2023 00:00:00 +0100},
  biburl = {https://dblp.org/rec/conf/apsec/TranBG020.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org},
}