The full list of publications can be consulted here (or more easily at DBLP or Google Scholar).


Safety Verification for Robotic Software, a COMPETE2020 project that aims to develop techniques to promote the verification of safety critical properties for robotic software controllers.
Trustworthy Software Design with Alloy, a COMPETE2020 project that aims to develop a methodology for trustworthy software design that is both formal, unified, and lightweight around Alloy.
Collaborative Laboratory on Cyber Physical Systems and Cyber Security​, aiming to create skilled jobs and economic and social value, by promoting employment through the development of knowledge-based activities.


An ORCID-based Synchronization Framework for the Portuguese CRIS, a project commissioned by FCT that aims to develop a synchronization framework for information exchange between the various national systems and international systems.
Demonstration of INTElligent grid technologies for renewables INTEgration and INTEractive consumer participation enabling INTEroperable market solutions and INTErconnected stakeholders, an H2020 project that aims develop innovative solutions of smart grids.
High-Assurance Medical Cyber-physical Systems, a NORTE2020 project that aims to contribute to safer medical cyber-physical systems through the development of such design and analysis techniques.
Foundations, Applications and Tools for Bidirectional Transformation, a COMPETE project that aimed to propose effective bidirectional transformation frameworks for model-driven engineering, spreadsheet validation and transformation, and language-based editors defined with attribute grammars.
Languages and Tools for Critical Real-Time Systems, an ON.2 project that aimed to contribute to a change to the current paradigm of secure ITC infrastructure, according to which the deployment and operation of a critical system implies security enforcement as a reactive process.


Electrum Analyzer
is an extension of the Alloy Analyzer for the bounded and unbounded model checking of Electrum models.
is an extension of Kodkod with support for target-oriented, temporal and decomposed model finding with symbolic bounds.
is a web application for the online editing and sharing of Alloy models and instances, including simple specification challenges.
is an ORCID-based synchronization framework for CRIS's developed following formal methodologies.
is an Eclipse plug-in to operationalize QVT-R bidirectional model transformations using Alloy.


André Santos
Co-supervision of the PhD thesis on "High-assurance Robotics Software".
Chong Liu
Co-supervision of the PhD thesis on "Lightweight Trustworthy High-level Software Design".
Renato Carvalho
Supervision of the MSc thesis on the "Analysis of Message Passing Software using Electrum".
Gonçalo Duarte
Supervision of the MSc thesis on the "Application of Formal Analysis Techniques to Robotic Software".
Patrícia Barreira
Co-supervision of the MSc thesis on "A Formal Methods Perspective on NoSQL Distributed Transactions".
Pedro Silva
Co-supervision of the MSc thesis "Towards a Quantitative Alloy".


Eduardo Pessoa
Supervision of the MSc thesis on "Parallel Verification of Dynamic Systems with Rich Configurations".
José Pereira
Co-supervision of the MSc thesis on "A Web-based Social Environment for Alloy".
André Santos
Co-supervision of the MSc thesis on "Applying Coding Standards to the Robot Operating System".
Miguel Costa
Co-supervision of the MSc thesis on "Software Quality for the Robot Operating System".


Formal Methods in Software Engineering (MFES)
MSc, Fall 2020 (MIEIC@FEUP)
Fundaments of Programming (FPRO)
BSc, Fall 2020 (MIEIC@FEUP)
Program Calculation (CP)
BSc, Spring 2020 (MIEI@UM)
Specification and Modelling (EM)
MSc, Fall 2015, 2018, 2019 (MIEI+MCC@UM)
Computer Labs I (LI1)
BSc, Fall 2009, 2011, 2012, 2015 - 2017, 2019 (MIEI@UM)
Imperative Programming (PI)
BSc, Spring 2018 (MIEI@UM), 2019 (MIEI+LCC+MIEFis@UM)
Functional Programming (PF)
BSc, Fall 2016 (LCC+MIEFis@UM), 2017 (MIEI@UM)
Applied Informatics (LAD)
BSc, Spring 2017 (LLA@UM)
Software Development Labs (LDS)
BSc, Fall 2013 (LEI@IPP)
Checkout the LI1@UM Hall of Fame with the best student projects since 2013.