go2pins: A model checking toolset for the Go programming language

From LRDE

Revision as of 19:58, 7 June 2018 by Bot (talk | contribs)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)

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.