This artifact contains a version of the Godel tool that checks MiGo+ types – an extension of MiGo from [1] 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 [1]. This new version adds the ability to extract shared memory pointers as well as Mutex and RWMutex locks.

[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: http://doi.acm.org/10.1145/3180155.3180157, doi:10.1145/3180155.3180157.