Difference between revisions of "Publications/kirszenberg.21.spin"
From LRDE
(Created page with "{{Publication | published = true | date = 2021-02-16 | authors = Alexandre Kirszenberg, Antoine Martin, Hugo Moreau, Etienne Renault | title = Go2Pins: a framework for the LTL...") |
|||
Line 1: | Line 1: | ||
{{Publication |
{{Publication |
||
| published = true |
| published = true |
||
− | | date = 2021- |
+ | | date = 2021-06-08 |
| authors = Alexandre Kirszenberg, Antoine Martin, Hugo Moreau, Etienne Renault |
| authors = Alexandre Kirszenberg, Antoine Martin, Hugo Moreau, Etienne Renault |
||
| title = Go2Pins: a framework for the LTL verification of Go programs |
| title = Go2Pins: a framework for the LTL verification of Go programs |
||
Line 12: | Line 12: | ||
| lrdepaper = http://www.lrde.epita.fr/dload/papers/kirszenberg.21.spin.pdf |
| lrdepaper = http://www.lrde.epita.fr/dload/papers/kirszenberg.21.spin.pdf |
||
| lrdekeywords = Spot |
| lrdekeywords = Spot |
||
− | | lrdenewsdate = 2021- |
+ | | lrdenewsdate = 2021-06-08 |
| type = inproceedings |
| type = inproceedings |
||
| id = kirszenberg.21.spin |
| id = kirszenberg.21.spin |
||
− | | identifier = doi: |
+ | | identifier = doi:?? |
| bibtex = |
| bibtex = |
||
@InProceedings<nowiki>{</nowiki> kirszenberg.21.spin, |
@InProceedings<nowiki>{</nowiki> kirszenberg.21.spin, |
||
Line 45: | Line 45: | ||
early stages of development, our results are promising and |
early stages of development, our results are promising and |
||
show the the benefits of using black-box transitions.<nowiki>}</nowiki>, |
show the the benefits of using black-box transitions.<nowiki>}</nowiki>, |
||
− | doi = <nowiki>{</nowiki> |
+ | doi = <nowiki>{</nowiki>??<nowiki>}</nowiki> |
<nowiki>}</nowiki> |
<nowiki>}</nowiki> |
||
Revision as of 08:45, 8 June 2021
- 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
- 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
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 = {??} }