Skip to main content

Hello! My name is Lina Marsso.

I am currently an assistant professor, at the computer science department of Polytechnique Montréal, and associate academic member at MILA.


lina [dot] marsso [at] polymtl [dot] ca

Research goal

My long-term research goal is to enable the development of autonomous systems that are safe and responsible.     Specifically, I aim to answer the following questions: What exactly does it mean for an autonomous 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.

Educational Background

I was a post-doctoral researcher in the Department of Computer Science at the University of Toronto in the Modelling and Verification group, with Professor Marsha Chechik. 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.     

Interested in working together with me?

Feel free to contact me!

RE4AI

I am particularly interested in the elicitation of requirements for safe and  trustworthy AI systems. Please take a look at my RETRAI workshop.

SE4AI

Given the elicited requirements, I am also exploring software‑engineering techniques to validate and guide AI‑based systems so

they become trustworthy.

FM

I am also interested in developing and applying formal methods to software in general, including systems with AI components.

Publications

For the complete list [click here (DBLP)]         
  • LEGOS-SLEEC: Tool for Formalizing and Analyzing Normative Requirements
    Kevin Kolyakov, Lina Marsso, Nick Feng, Junwei Quan, and Marsha Chechik (short paper).  Proceedings of the 47th International Conference on Software Engineering ICSE/DEMO'2025 (Ottawa, Canada), 2025  
    (Tool, Video).     
  • Diagnosis via Proofs of Unsatisfiability for First-Order Logic with Relational Objects
    Nick Feng, Lina Marsso, and Marsha Chechik.  Proceedings of the 39th International Conference on Automated Software Engineering ASE'2024, (Sacramento, California, United States), 2024        
    (Paper, Tool, Slides).     
  • Normative Requirements Operationalization with Large Language Models
    Nick Feng, Lina Marsso, Sinem Getir Yaman, Isobel Standen, Yesugen Baatartogtokh, Reem Ayad, Victória Oldemburgo de Mello, Beverley Townsend, Hanne Bartels, Ana Cavalcanti, Radu Calinescu, and Marsha Chechik.  Proceedings of the 32nd IEEE International Requirements Engineering  RE'2024 (Reykjavik, Iceland), 2024        
    (Paper, Tool, Slides).     
  • Analyzing and Debugging Normative Requirements via Satisfiability Checking
    Nick Feng, Lina Marsso, Sinem Getir Yaman, Beverley Townsend, Yesugen Baatartogtokh, Reem Ayad, Victória Oldemburgo de Mello, 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, Slides).     
  • Towards a Formal Framework for Normative Requirements Elicitation
    Nick Feng, Lina Marsso, Sinem Getir-Yaman, Townsend Beverley, Radu Calinescu, Ana Cavalcanti, and Marsha Chechik (short paper).  Proceedings of the 38th International Conference on Automated Software Engineering ASE/NIER'23 (Kirchberg, Luxembourg), 2023        
    (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        
    (Paper, Material).     
  • 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).     

    • Contact

    lina [dot] marsso [at] polymtl [dot] ca