Static Race Detection and Mutex Safety and Liveness for Go Programs (Artifact)

Authors Julia Gabet , Nobuko Yoshida

Thumbnail PDF

Artifact Description

  • Filesize: 375 kB
  • 3 pages

Document Identifiers

Author Details

Julia Gabet
  • Imperial College London, United Kingdom
Nobuko Yoshida
  • Imperial College London, United Kingdom


The authors wish to thank Nicholas Ng for his initial collaboration on the project, David Castro-Perez and Fangyi Zhou for their comments and testing the artifact, and the anonymous reviewers for their comments and suggestions.

Cite AsGet BibTex

Julia Gabet and Nobuko Yoshida. Static Race Detection and Mutex Safety and Liveness for Go Programs (Artifact). In Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020). Dagstuhl Artifacts Series (DARTS), Volume 6, Issue 2, pp. 12:1-12:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)



This artifact contains a version of the Godel tool that checks MiGo+ types - an extension of MiGo from [Lange et al., 2018] including GoL. Given the extracted MiGo+ types, the tool can analyse them using the mCRL2 model checker to check several properties including liveness, safety and data race freedom as defined in our paper. The artifact also includes examples, shipped with both the source of the Godel tool and the benchmark repository. The latter also contains the Go source for the benchmark examples. We provide compiled binaries of the artifact in a Docker image, with instructions on how to use them. Finally, for convenience, the Docker image also contains a binary version of the migoinfer+ tool, developed as a fork from the original migoinfer by Nicholas Ng in [Lange et al., 2018]. This new version adds the ability to extract shared memory pointers as well as Mutex and RWMutex locks.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Concurrent programming languages
  • Software and its engineering → Model checking
  • Theory of computation → Process calculi
  • Go language
  • behavioural types
  • race detection
  • happens-before relation
  • safety
  • liveness


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Julien Lange, Nicholas Ng, Bernardo Toninho, and Nobuko Yoshida. A static verification framework for message passing in go using behavioural types. In Proceedings of the 40th International Conference on Software Engineering, ICSE '18, pages 1137-1148, New York, NY, USA, 2018. ACM. URL: