Lina Marsso
Email:
lina (dot) marsso (at) inria (dot) fr
Address:
Inria Grenoble - Rhône-Alpes
655, avenue de l'Europe
Montbonnot Saint-Martin
38334 SAINT-ISMIER CEDEX
FRANCE
About
I am currently doing a post-doc at the University of Toronto in the group of Marsha Chechik. Please see my current Web page.
I was a PhD student member of the CONVECS project-team (Inria Grenoble - Rhône-Alpes and LIG).
I defended in December 2019 my PhD thesis, entitled "On Model-based Testing of GALS Systems", under the supervision of Radu Mateescu, Ioannis Parissis, and Wendelin Serwe.
I received an MSc degree in computer science in 2016 from the University of Grenoble.
During my PhD, I developed new methods to automate test generation for Globally Asynchronous Locally Synchronous (GALS) systems.
This involved the formal modeling of GALS applications, the exploration of the models on the fly, as well as the integration of synchronous and asynchronous testing techniques.
My research interests include formal methods, process algebra,
model-based testing, program analysis and verification.
Publications
For my recent publications [click here (DBLP)]
-
Specifying a Cryptographical Protocol in Lustre and SCADE
Lina Marsso.
Proceedings of the 4th Workshop on Models for Formal Analysis of Real Systems MARS'2020 (Dublin, Ireland), 2020
(Paper).
-
Asynchronous Testing of Synchronous Components in GALS Systems
Lina Marsso, Radu Mateescu, Ioannis Parissis, and Wendelin Serwe.
Proceedings of the 15th International Conference on integrated Formal Methods IFM'2019 (Bergen, Norway), December 2-6, 2019
(Paper, Slides).
-
TESTOR: A Modular Tool for On-the-Fly Conformance Test Case Generation
Lina Marsso, Radu Mateescu, and Wendelin Serwe.
Proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS'2018 (Thessaloniki, Greece), April 14-20, 2018
(Paper, Slides).
-
Comparative Study of Eight Formal Specifications of the Message Authenticator Algorithm
Hubert Garavel and Lina Marsso.
Proceedings of the 3rd Workshop on Models for Formal Analysis of Real Systems and the 6th International Workshop on Verification and Program Transformation MARS/VPT'2018 (Thessaloniki, Greece), April 20, 2018
(Paper, Slides).
-
A Formal TLS Handshake Model in LNT
Josip Bozic, Lina Marsso, Radu Mateescu, and Franz Wotawa.
Proceedings of the 3rd Workshop on Models for Formal Analysis of Real Systems and the 6th International Workshop on Verification and Program Transformation MARS/VPT'2018 (Thessaloniki, Greece), April 20, 2018
(Paper, Slides).
-
A Large Term Rewrite System Modelling a Pioneering Cryptographic Algorithm
Hubert Garavel and Lina Marsso.
Proceedings of the 2nd Workshop on Models for Formal Analysis of Real Systems MARS'2017 (Uppsala, Sweden), April 29, 2017
(Paper, Slides).
Formal models
-
Message Authenticator Algorithms:
I reconsidered the formalisation of a message authentication algorithm (MAA), in collaboration with Hubert Garavel.
We formalized the MAA in LNT, LOTOS and term rewrite system (in the REC language), and used the CADP toolbox to check our models.
I also formalized the MAA in LUSTRE and SCADE, and used the LURETTE and SCADE tools to test these models.
-
The Transport Layer Security (TLS) Protocol Version 1.3:
As part of a Hubert Curien partnership (PHC Amadeus program of Campus France, RIDINGS), with my team, we are collaborating with the Graz Institute of Software Technology in Austria.
With my colleagues from IST Graz, I worked on the formalization in LNT, and validation of the first formal model of the Draft TLS 1.3 handshake protocol for securing exchanges on the Internet.