Difference between revisions of "Publications/renault.22.sttt"
From LRDE
| (One intermediate revision by the same user not shown) | |||
| Line 5: | Line 5: | ||
| title = Go2Pins: A framework for the LTL verification of Go programs (Extended Version) |
| title = Go2Pins: A framework for the LTL verification of Go programs (Extended Version) |
||
| journal = International Journal on Software Tools for Technology Transfer (STTT) |
| journal = International Journal on Software Tools for Technology Transfer (STTT) |
||
| − | | |
+ | | volume = 25 |
| − | | |
+ | | pages = 77 to 94 |
| − | | optpages = ???–??? |
||
| − | | optmonth = ??? |
||
| publisher = Springer |
| publisher = Springer |
||
| lrdeprojects = Spot |
| lrdeprojects = Spot |
||
| Line 14: | Line 12: | ||
| abstract = We introduce Go2Pins, a tool that takes a program written in Go and links it with two model-checkers: LTSMin and Spot. Go2Pins is an effort to promote the integration of both formal verification 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 verification techniques, allows easy, automatic and efficient abstractions. Go2Pins also handles basic concurrent programs through the use of a dedicated scheduler. Moreover, in order to efficiently handle recursive programs, we introduce PSLRec, a formalism that augments PSL without changing the complexity of the underlying verification process. |
| abstract = We introduce Go2Pins, a tool that takes a program written in Go and links it with two model-checkers: LTSMin and Spot. Go2Pins is an effort to promote the integration of both formal verification 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 verification techniques, allows easy, automatic and efficient abstractions. Go2Pins also handles basic concurrent programs through the use of a dedicated scheduler. Moreover, in order to efficiently handle recursive programs, we introduce PSLRec, a formalism that augments PSL without changing the complexity of the underlying verification process. |
||
| lrdepaper = http://www.lrde.epita.fr/dload/papers/renault.22.sttt.pdf |
| lrdepaper = http://www.lrde.epita.fr/dload/papers/renault.22.sttt.pdf |
||
| + | | note = First published online on 06 January 2023. |
||
| − | | optdoi = ??? |
||
| type = article |
| type = article |
||
| id = renault.22.sttt |
| id = renault.22.sttt |
||
| + | | identifier = doi:https://doi.org/10.1007/s10009-022-00692-w |
||
| bibtex = |
| bibtex = |
||
@Article<nowiki>{</nowiki> renault.22.sttt, |
@Article<nowiki>{</nowiki> renault.22.sttt, |
||
| Line 25: | Line 24: | ||
journal = <nowiki>{</nowiki>International Journal on Software Tools for Technology |
journal = <nowiki>{</nowiki>International Journal on Software Tools for Technology |
||
Transfer (STTT)<nowiki>}</nowiki>, |
Transfer (STTT)<nowiki>}</nowiki>, |
||
| − | year = |
+ | year = 2023, |
| − | + | volume = <nowiki>{</nowiki>25<nowiki>}</nowiki>, |
|
| − | + | pages = <nowiki>{</nowiki>77--94<nowiki>}</nowiki>, |
|
| + | month = feb, |
||
| ⚫ | |||
| − | optmonth = <nowiki>{</nowiki>???<nowiki>}</nowiki>, |
||
publisher = <nowiki>{</nowiki>Springer<nowiki>}</nowiki>, |
publisher = <nowiki>{</nowiki>Springer<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 |
||
| Line 45: | Line 43: | ||
augments PSL without changing the complexity of the |
augments PSL without changing the complexity of the |
||
underlying verification process.<nowiki>}</nowiki>, |
underlying verification process.<nowiki>}</nowiki>, |
||
| − | + | doi = <nowiki>{</nowiki>https://doi.org/10.1007/s10009-022-00692-w<nowiki>}</nowiki>, |
|
| ⚫ | |||
<nowiki>}</nowiki> |
<nowiki>}</nowiki> |
||
Latest revision as of 18:49, 10 March 2023
- Authors
- Alexandre Kirszenberg, Antoine Martin, Hugo Moreau, Etienne Renault
- Journal
- International Journal on Software Tools for Technology Transfer (STTT)
- Type
- article
- Publisher
- Springer
- Projects
- Spot
- Date
- 2022-12-09
Abstract
We introduce Go2Pins, a tool that takes a program written in Go and links it with two model-checkers: LTSMin and Spot. Go2Pins is an effort to promote the integration of both formal verification 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 verification techniques, allows easy, automatic and efficient abstractions. Go2Pins also handles basic concurrent programs through the use of a dedicated scheduler. Moreover, in order to efficiently handle recursive programs, we introduce PSLRec, a formalism that augments PSL without changing the complexity of the underlying verification process.
Documents
Bibtex (lrde.bib)
@Article{ renault.22.sttt,
author = {Alexandre Kirszenberg and Antoine Martin and Hugo Moreau
and Etienne Renault},
title = {Go2{P}ins: {A} framework for the {LTL} verification of
{Go} programs (Extended Version)},
journal = {International Journal on Software Tools for Technology
Transfer (STTT)},
year = 2023,
volume = {25},
pages = {77--94},
month = feb,
publisher = {Springer},
abstract = {We introduce Go2Pins, a tool that takes a program written
in Go and links it with two model-checkers: LTSMin and
Spot. Go2Pins is an effort to promote the integration of
both formal verification 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 verification techniques, allows easy, automatic
and efficient abstractions. Go2Pins also handles basic
concurrent programs through the use of a dedicated
scheduler. Moreover, in order to efficiently handle
recursive programs, we introduce PSL{Rec}, a formalism that
augments PSL without changing the complexity of the
underlying verification process.},
doi = {https://doi.org/10.1007/s10009-022-00692-w},
note = {First published online on 06 January 2023.}
}