Go2Pins: A Framework for the LTL Verification of Go Programs

Authors

Alexandre Kirszenberg, Antoine Martin, Hugo Moreau, Etienne Renault

Where

Proceedings of the 27th International SPIN Symposium on Model Checking of Software (SPIN'21)

Place

Aarhus, Denmark (online)

Type

inproceedings

Publisher

Springer, Cham

Keywords

Spot

Date

2021-06-08

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

• Paper

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},
  volume	= {12864},
  month		= may,
  address	= {Aarhus, Denmark (online)},
  publisher	= {Springer, Cham},
  pages		= {140--156},
  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		= {10.1007/978-3-030-84629-9_8}
}