Handling blackbox transitions in go2pins

Authors

Hugo Moreau

Type

techreport

Year

2021

Number

2108

Abstract

go2pins is a tool used to interface Go programs with model checking algorithms. Through a series of transformations, a standard Go program is compiled to another behaving the same way, but exposing an interface allowing to iterate over its various states. We introduce black-box transitions, an efficient and scalable technique for handling the Go runtime. This approachinspired from the hardware verification techniques, allows easy, automatic and efficient abstractions. In this reportwe introduce the development behind the introduction of the black-box transitions in textttgo2pins and the problems encountered.