Difference between revisions of "Publications/kirszenberg.21.spin"
From LRDE
Line 3: | Line 3: | ||
| date = 2021-06-08 |
| date = 2021-06-08 |
||
| authors = Alexandre Kirszenberg, Antoine Martin, Hugo Moreau, Etienne Renault |
| authors = Alexandre Kirszenberg, Antoine Martin, Hugo Moreau, Etienne Renault |
||
− | | title = Go2Pins: |
+ | | 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) |
| booktitle = Proceedings of the 27th International SPIN Symposium on Model Checking of Software (SPIN'21) |
||
| series = Lecture Notes in Computer Science |
| series = Lecture Notes in Computer Science |
||
+ | | volume = 12864 |
||
− | | address = Aarhus, |
+ | | address = Aarhus, Denmark (online) |
− | | publisher = Springer |
||
− | | |
+ | | publisher = Springer, Cham |
+ | | pages = 140 to 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 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. |
| 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. |
||
| lrdepaper = http://www.lrde.epita.fr/dload/papers/kirszenberg.21.spin.pdf |
| lrdepaper = http://www.lrde.epita.fr/dload/papers/kirszenberg.21.spin.pdf |
||
Line 15: | Line 16: | ||
| type = inproceedings |
| type = inproceedings |
||
| id = kirszenberg.21.spin |
| id = kirszenberg.21.spin |
||
− | | identifier = doi: |
+ | | identifier = doi:10.1007/978-3-030-84629-9_8 |
| bibtex = |
| bibtex = |
||
@InProceedings<nowiki>{</nowiki> kirszenberg.21.spin, |
@InProceedings<nowiki>{</nowiki> kirszenberg.21.spin, |
||
author = <nowiki>{</nowiki>Alexandre Kirszenberg and Antoine Martin and Hugo Moreau |
author = <nowiki>{</nowiki>Alexandre Kirszenberg and Antoine Martin and Hugo Moreau |
||
and Etienne Renault<nowiki>}</nowiki>, |
and Etienne Renault<nowiki>}</nowiki>, |
||
− | title = <nowiki>{</nowiki>Go2Pins: |
+ | title = <nowiki>{</nowiki><nowiki>{</nowiki>Go2Pins<nowiki>}</nowiki>: <nowiki>{</nowiki>A<nowiki>}</nowiki> Framework for the <nowiki>{</nowiki>LTL<nowiki>}</nowiki> Verification of |
− | + | <nowiki>{</nowiki>Go<nowiki>}</nowiki> Programs<nowiki>}</nowiki>, |
|
booktitle = <nowiki>{</nowiki>Proceedings of the 27th International SPIN Symposium on |
booktitle = <nowiki>{</nowiki>Proceedings of the 27th International SPIN Symposium on |
||
Model Checking of Software (SPIN'21)<nowiki>}</nowiki>, |
Model Checking of Software (SPIN'21)<nowiki>}</nowiki>, |
||
year = <nowiki>{</nowiki>2021<nowiki>}</nowiki>, |
year = <nowiki>{</nowiki>2021<nowiki>}</nowiki>, |
||
series = <nowiki>{</nowiki>Lecture Notes in Computer Science<nowiki>}</nowiki>, |
series = <nowiki>{</nowiki>Lecture Notes in Computer Science<nowiki>}</nowiki>, |
||
+ | volume = <nowiki>{</nowiki>12864<nowiki>}</nowiki>, |
||
month = may, |
month = may, |
||
address = <nowiki>{</nowiki>Aarhus, Denmark (online)<nowiki>}</nowiki>, |
address = <nowiki>{</nowiki>Aarhus, Denmark (online)<nowiki>}</nowiki>, |
||
− | publisher = <nowiki>{</nowiki>Springer<nowiki>}</nowiki>, |
+ | publisher = <nowiki>{</nowiki>Springer, Cham<nowiki>}</nowiki>, |
− | pages = <nowiki>{</nowiki> |
+ | pages = <nowiki>{</nowiki>140--156<nowiki>}</nowiki>, |
abstract = <nowiki>{</nowiki>We introduce Go2Pins, a tool that takes a program written |
abstract = <nowiki>{</nowiki>We introduce Go2Pins, a tool that takes a program written |
||
in Go and links it with two model-checkers: LTSMin [19] and |
in Go and links it with two model-checkers: LTSMin [19] and |
||
Line 45: | Line 47: | ||
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>10.1007/978-3-030-84629-9_8<nowiki>}</nowiki> |
<nowiki>}</nowiki> |
<nowiki>}</nowiki> |
||
Latest revision as of 15:06, 6 September 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, 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
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} }