Go2Pins: a framework for the LTL verification of Go programs

From LRDE

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 approachinspired 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.

Documents

Bibtex (lrde.bib)

@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		= {??}
}