Research goal

My long-term research goal is to enable the development of intelligent systems that are safe and responsible. Specifically, I aim to answer the following questions: What exactly does it mean for an intelligent system to be safe and responsible? How can we develop approaches that assess whether such systems comply with established standards? Finally, when a system fails to comply, how can we adapt its behaviour to meet the defined standards? To answer these questions, I integrate formal methods with software engineering techniques.

Current Research Activities

• Formal conformance testing
• Satisfiability checking
• Verifying reliability of perception components
• Analyzing reliability of machine learning models
• Formalisation and verification of social, legal, ethical, empathetic, and cultural (SLEEC) requirements
• Monitoring compliance of SLEEC requirements

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)]

• Analyzing and Debugging Normative Requirements via Satisfiability Checking
  Nick Feng, Lina Marsso, Sinem Getir Yaman, Bev Townsend, Yesugen Baatartogtokh, Reem Ayad, Victória Oldemburgo de Mello, Yuliia Kholodetska, Isobel Standen, Ioannis Stefanakos, Calum Imrie, Genaina Rodrigues, Ana Cavalcanti, Radu Calinescu, and Marsha Chechik. ACM SIGSOFT Distinguished Paper Award. Proceedings of the 46th International Conference on Software Engineering ICSE'2024 (Lisboa, Portugal), 2024
  (Paper, Tool, Case-studies).
• Towards a Formal Framework for Normative Requirements Elicitation
  Nick Feng, Lina Marsso, Sinem Getir-Yaman, Townsend Beverley, Radu Calinescu, Ana Cavalcanti, Marsha Chechik (short paper). Proceedings of the 38th International Conference on Automated Software Engineering, (ASE/NIER'23), Kirchberg, Luxembourg
  (Paper, Slides, Tool).
• Early Verification of Legal Compliance via Bounded Satisfiability Checking
  Nick Feng, Lina Marsso, Mehrdad Sabetzadeh, Marsha Chechik. Proceedings of the 34th International Conference on Computer-Aided Verification CAV'23 (Paris, France), 2023
  (Extended paper, Tool).
• 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'22) (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

  I have formalised two behavioral models of an autonomous vehicle (AV) and its interaction with the environment, in collaboration with Lucie Muller, Radu Mateescu, and Wendelin Serwe. The first model is used to validate the overall AV, and the second model is used to validate the perception component via autonomous driving scenarios generation and testing. Both models are formalised in LNT, and we used the CADP toolbox to check them.

• 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

• ICSE'25 (Programme committee member in the 47th International Conference on Software Engineering, Research Track.)
• FMICS'24 (Programme committee member in the 29th International Conference on Formal Methods for Industrial Critical Systems.)
• NFM'24 (Programme committee member in the 16th NASA Formal Methods Symposium.)
• MARS'24-22 (Programme committee member in the 6th Workshop on Models for Formal Analysis of Real Systems)
• SE4SafeML'2023 (Organizer of the 1rst International Workshop on Dependability and Trustworthiness of Safety-Critical Systems with Machine Learned Components)
• FASE'23 (Programme committee member in the 26th International Conference on Fundamental Approaches to Software Engineering)
• FTSCS'22-23 (Programme committee member in the Workshop on Formal Techniques for Safety-Critical Systems)
• MACTA-23 (Programme committee member in the Workshop on Multidisciplinary Approaches to Co-Creating Trustworthy Autonomous Systems)
• FMAS'23-22-21 (Programme committee member in the Workshop on Formal Methods for Autonomous Systems)
• SEFM'19 (Publicity chair in the 17th International Conference on Software Engineering and Formal Methods)

Pro Bono Office Hours

I allocate time each week to provide guidance, advice, or mentorship to students in need, especially those from underrepresented groups. If you're interested, please contact me (lina (dot) marsso (at) utoronto (dot) ca).