Go2Pins: a framework for the LTL verification of Go programs (extended version)

We introduce Go2Pins, a tool that takes a program written in Go and links it with two model checkers: LTSMin (Kant et al. Ltsmin: high-performance language-independent model checking. In: TACAS'15, pp. 692-707, 2015) and Spot (Duret-Lutz et al. Spot 2.0-a framework for LTL and omega automata manipulation. In: ATVA'16, vol. 9938 of LNCS, pp. 1294, 122-129, 2016) . 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. Moreover, in order to efficiently handle recursive programs, we introduce PSLREC, a formalism that augments PSL without changing the complexity of the underlying verification process. 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 benefits of using black-box transitions. This paper also shows how Go2Pins is able to work efficiently on two bugs coming from industrial problems Kubernetes and Trillian.