New publication: SPIN'21 - Annonce

10 Jun 2021


      Greetings,
We are pleased to announce that the following paper has been accepted to the
27th International SPIN Symposium on Model Checking of Software (SPIN'21)
that will take place online, on the 12-13th of July 202.
Title and corresponding authors:
"Go2Pins: a framework for the LTL verification 
    			  of Go programs"
Alexandre Kirszenberg(1) and Antoine Martin(1) and 
     	Hugo Moreau(1) and Etienne Renault(1)
(1) LRDE, EPITA, Le Kremlin-Bicêtre, France
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 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.  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.
More information at :
    https://www.lrde.epita.fr/wiki/Publications/kirszenberg.21.spin https://www.lrde.epita.fr/wiki/Publications/kirszenberg.21.spin