We introduce Go2Pins, a tool that takes a program written in Go and
links it with two model-checkers: LTSMin [19] and Spot [7]. Go2Pins is
an effort to promote the integration of both formal verification and
testing inside industrial-size projects. With this goal in mind, we
introduce black-box transitions, an efficient and scalable technique
for handling the Go runtime. This approach, inspired by hardware
verification techniques, allows easy, automatic and efficient
abstractions. Go2Pins also handles basic concurrent programs through
the use of a dedicated scheduler. In this paper we demonstrate the
usage of Go2Pins over benchmarks inspired by industrial problems and a
set of LTL formulae. Even if Go2Pins is still at the early stages of
development, our results are promising and show the the benefits of
using black-box transitions.
More information at :