Difference between revisions of "Publications/renault.22.sttt"
From LRDE
Line 3: | Line 3: | ||
| date = 2022-12-09 |
| date = 2022-12-09 |
||
| authors = Etienne Renault, Alexandre Duret-Lutz, Fabrice Kordon, Denis Poitrenaud |
| authors = Etienne Renault, Alexandre Duret-Lutz, Fabrice Kordon, Denis Poitrenaud |
||
− | | title = Go2Pins: |
+ | | 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 = ??? |
| volume = ??? |
||
Line 11: | Line 11: | ||
| lrdeprojects = Spot |
| lrdeprojects = Spot |
||
| lrdenewsdate = 2022-12-09 |
| lrdenewsdate = 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. |
+ | | 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 |
||
| type = article |
| type = article |
||
Line 20: | Line 20: | ||
author = <nowiki>{</nowiki>Etienne Renault and Alexandre Duret-Lutz and Fabrice |
author = <nowiki>{</nowiki>Etienne Renault and Alexandre Duret-Lutz and Fabrice |
||
Kordon and Denis Poitrenaud<nowiki>}</nowiki>, |
Kordon and Denis Poitrenaud<nowiki>}</nowiki>, |
||
− | title = <nowiki>{</nowiki> |
+ | title = <nowiki>{</nowiki>Go2<nowiki>{</nowiki>P<nowiki>}</nowiki>ins: <nowiki>{</nowiki>A<nowiki>}</nowiki> framework for the <nowiki>{</nowiki>LTL<nowiki>}</nowiki> verification of |
− | programs (Extended Version)<nowiki>}</nowiki>, |
+ | <nowiki>{</nowiki>Go<nowiki>}</nowiki> programs (Extended Version)<nowiki>}</nowiki>, |
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>, |
||
Line 30: | Line 30: | ||
month = ???, |
month = ???, |
||
publisher = <nowiki>{</nowiki>Springer<nowiki>}</nowiki>, |
publisher = <nowiki>{</nowiki>Springer<nowiki>}</nowiki>, |
||
− | abstract = <nowiki>{</nowiki> |
+ | abstract = <nowiki>{</nowiki>We introduce Go2Pins, a tool that takes a program written |
in Go and links it with two model-checkers: LTSMin and |
in Go and links it with two model-checkers: LTSMin and |
||
Spot. Go2Pins is an effort to promote the integration of |
Spot. Go2Pins is an effort to promote the integration of |
Revision as of 23:23, 12 December 2022
- Authors
- Etienne Renault, Alexandre Duret-Lutz, Fabrice Kordon, Denis Poitrenaud
- 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 = {Etienne Renault and Alexandre Duret-Lutz and Fabrice Kordon and Denis Poitrenaud}, 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 = 2022, volume = ???, number = ???, pages = {???--???}, month = ???, 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 = {???} }