go2pins: A model checking toolset for the Go programming language

From LRDE

The printable version is no longer supported and may have rendering errors. Please update your browser bookmarks and please use the default browser print function instead.

Abstract

Model Checking is a set of techniques and algorithms for verifying that programs respect certain properties. In this report, we present a toolchain for applying existing model checking algorithms to Go programs. Through a set of transformations, we compile a Go program to an equivalent Go program whose state can be iterated upon. This new program exposes a standard interface to plug in to model checking solutions.