@InProceedings{   kirszenberg.21.spin,
  author        = {Alexandre Kirszenberg and Antoine Martin and Hugo Moreau
                  and Etienne Renault},
  title         = {Go2Pins: a framework for the LTL verification of Go programs},
  booktitle     = {Proceedings of the 27th International SPIN Symposium on Model
                   Checking of Software (SPIN'21)},
  year          = {2021},
  series        = {Lecture Notes in Computer Science},
  month         = may,
  address       = {Aarhus,  Denmark (online)},
  publisher     = {Springer},
  pages         = {??--??},
  abstract      = {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 verifica- tion 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 ver- ification 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.},
  doi           = {??}
}