Difference between revisions of "Publications/renault.22.sttt"

From LRDE

(Created page with "{{Publication | published = true | date = 2022-12-09 | authors = Etienne Renault, Alexandre Duret-Lutz, Fabrice Kordon, Denis Poitrenaud | title = Go2Pins: a framework for the...")
 
 
(5 intermediate revisions by the same user not shown)
Line 2: Line 2:
 
| published = true
  
| published = true
 
| date = 2022-12-09
  
| date = 2022-12-09
−
| authors = Etienne Renault, Alexandre Duret-Lutz, Fabrice Kordon, Denis Poitrenaud
 +
| authors = Alexandre Kirszenberg, Antoine Martin, Hugo Moreau, Etienne Renault
−
| 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 = ???
 +
| volume = 25
−
| number = ???
 +
| pages = 77 to 94
−
| pages = ??? to ???
  
 
| publisher = Springer
  
| publisher = Springer
 
| 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. This approachinspired by hardware verification techniques, allows easyautomatic 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
  +
| note = First published online on 06 January 2023.
 
| type = article
  
| type = article
 
| id = renault.22.sttt
  
| id = renault.22.sttt
−
| identifier = doi:???
 +
| 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,
−
author = <nowiki>{</nowiki>Etienne Renault and Alexandre Duret-Lutz and Fabrice
 +
author = <nowiki>{</nowiki>Alexandre Kirszenberg and Antoine Martin and Hugo Moreau
−
Kordon and Denis Poitrenaud<nowiki>}</nowiki>,
 +
and Etienne Renault<nowiki>}</nowiki>,
−
title = <nowiki>{</nowiki>Go2Pins: a framework for the LTL verification of Go
 +
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>,
−
year = 2022,
 +
year = 2023,
−
volume = ???,
 +
volume = <nowiki>{</nowiki>25<nowiki>}</nowiki>,
  ⚫
pages = <nowiki>{</nowiki>77--94<nowiki>}</nowiki>,
−
number = ???,
  
  ⚫
month = feb,
⚫
pages = <nowiki>{</nowiki>???--???<nowiki>}</nowiki>,
  
⚫
month = ???,
  
 
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
 
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
Line 43: 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>???<nowiki>}</nowiki>
 +
doi = <nowiki>{</nowiki>https://doi.org/10.1007/s10009-022-00692-w<nowiki>}</nowiki>,
  +
note = <nowiki>{</nowiki>First published online on 06 January 2023.<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.}
}





Retrieved from "https://www.lrde.epita.fr/index.php?title=Publications/renault.22.sttt&oldid=128429"