Current Research Activities

• Formal conformance testing
• Satisfiability checking
• Analyzing reliability of computer vision models
• Formalisation and verification of privacy properties

Educational Background

I did my PhD in the CONVECS team at Inria, under the supervision of Professor Radu Mateescu, Professor Ioannis Parissis, and Professor Wendelin Serwe. I defended in December 2019 my PhD thesis, entitled "On Model-based Testing of GALS Systems". I received an MSc degree in computer science in 2016 from the University of Grenoble and my bachelor degree in computer science in 2014 from the University of Strasbourg.

Publications

For the complete list [click here (DBLP)]

• Early Verification of Legal Compliance via Bounded Satisfiability Checking
  Nick Feng, Lina Marsso, Mehrdad Sabetzadeh, and Marsha Chechik. Proceedings of the 34th International Conference on Computer-Aided Verification CAV'23 (Paris, France), 2023
  (TBA).
• DecompoVision: Reliability Analysis of Machine Vision Components Through Decomposition and Reuse
  Caroline Hu, Lina Marsso, Nikita Dvornik, Huakun Shen, and Marsha Chechik. Proceedings of the European Software Engineering Conference and Symposium on the Foundations of Software Engineering ESEC/FSE'23 (San Francisco, California, United States), 2023
  (TBA).
• Verifying Collision Risk Estimation using Autonomous Driving Scenarios Derived from a Formal Model
  Jean-Baptiste Horel, Philippe Ledent, Lina Marsso, Lucie Muller, Christian Laugier, Radu Mateescu, Anshul Paigwar, Alessandro Renzaglia, and Wendelin Serwe. Journal Intelligent and Robotic Systems, 2023
  (Paper, Scenarios).
• What to Check: Systematic Selection of Transformations for Analyzing Reliability of Machine Vision Components
  Caroline Hu, Lina Marsso, Krzysztof Czarnecki, and Marsha Chechik. Proceedings of the International Symposium on Software Reliability Engineering ISSRE'2022 (Charlotte, North Carolina, USA), 2022
  (Paper, Video, Material).
• If a Human Can See It, So Should Your System: Reliability Requirements for Machine Vision Components
  Caroline Hu, Lina Marsso, Krzysztof Czarnecki, Rick Salay, Huakun Shen, and Marsha Chechik. Proceedings of the 44th International Conference on Software Engineering ICSE'2022 (Pittsburgh, USA), 2022
  (Paper, Slides, Video, Material).
• Formally Modeling Autonomous Vehicles in LNT for Simulation and Testing
  Lina Marsso, Radu Mateescu, Lucie Muller, and Wendelin Serwe. Proceedings of the 5th Workshop on Models for Formal Analysis of Real Systems (Munich, Berlin), April 2, 2022
  (Paper, Models).
• Using Formal Conformance Testing to Generate Scenarios for Autonomous Vehicles
  Jean-Baptiste Horel, Christian Laugier, Lina Marsso, Radu Mateescu, Lucie Muller, Anshul Paigwar, Alessandro Renzaglia, and Wendelin Serwe. Proceedings of the 25th International Conference on Design, Automation & Test in Europe: Autonomous Systems Design DATE ASD'2022 (Antwere, Belgium), 2022
  (Paper).
• Automated Transition Coverage in Behavioural Conformance Testing
  Lina Marsso, Radu Mateescu, and Wendelin Serwe. Proceedings of the 32nd International Conference on Testing Software and Systems ICTSS'2020 (Naples, Italy), 2020
  (Paper).
• On Model-based Testing of GALS Systems
  Lina Marsso. PhD Thesis, Université Grenoble Alpes, December 10, 2019
  (Thesis).
• 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, Tool).
• 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,Models).
• 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, Model).

Formal models

• Autonomous Vehicles in LNT for Simulation and Testing

  COMING SOON

• 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 the INRIA team CONVECS, we were 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.

Academic Service

• SE4SafeML'2023 (Organizer of the 1rst International Workshop on Dependability and Trustworthiness of Safety-Critical Systems with Machine Learned Components)
• MACTA-23 (Programme committee member in the Workshop on Multidisciplinary Approaches to Co-Creating Trustworthy Autonomous Systems)
• FASE'23 (Programme committee member in the 26th International Conference on Fundamental Approaches to Software Engineering)
• FMAS'23-22-21 (Programme committee member in the Workshop on Formal Methods for Autonomous Systems)
• FTSCS'2022 (Programme committee member in the Workshop on Formal Techniques for Safety-Critical Systems)
• MARS'2022 (Programme committee member in the 5th Workshop on Models for Formal Analysis of Real Systems)
• SEFM'19 (Publicity chair in the 17th International Conference on Software Engineering and Formal Methods)