SELECTED PUBLICATIONS

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

PROJECTS

SpecRep
Constraint-based Specification Repair, an FCT exploratory project that aims to develop techniques to support the automatic repair of faulty specifications.
DLR
DigiLightRail, a platform for the verification of railway topological design models.
VORTEX
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.
SAFER
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.
TRUST
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.
PTCRIS
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.
InteGrid
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.
NanoSTIMA RL1.3
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.
FATBIT
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.
BEST CASE RL8
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.

SOFTWARE

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

CURRENT STUDENTS

Pedro Silva
Supervision of the PhD thesis on "High-level quantitative relational model finding".
Miguel Montes
Supervision of the MSc thesis on "Verifying hyperproperties with Alloy".
Tomás Maciel
Supervision of the MSc thesis on "Validating generative AI outputs though co-generation of code and specifications".

PAST STUDENTS

Gédsimon Pereira
Supervision of the MSc thesis on "Stateful security testing of web APIs".
Rui Gonçalves
Co-supervision of the MSc thesis on "Security verification for trustworthy software design".
Henrique Neto
Co-supervision of the MSc thesis on "Mining hints for fixing formal specifications".
Alexandre Abreu
Supervision of the MSc thesis on "Automatic specification repair in contract programming".
Ana Barros
Supervision of the MSc thesis on "Data-driven hint generation for Alloy using historical student submissions".
Gonçalo Teixeira
Co-supervision of the MSc thesis on "Security testing of web APIs".
Jorge Cerqueira
Co-supervision of the MSc thesis on "Automatic repair of behavioural specifications".
Chong Liu
Supervision of the PhD thesis on "Lightweight trustworthy high-level software design".
André Santos
Supervision of the PhD thesis on "High-assurance robotics software".
Rafael Moura
Supervision of the MSc thesis on "Graph databases for HR relationships".
Pedro Silva
Co-supervision of the MSc thesis on "Towards a quantitative Alloy".
Renato Carvalho
Supervision of the MSc thesis on "Analysis of message passing software using Electrum".
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".

ACTIVITIES

SBLP '22, '23, '25
PC member.
IEEE IRC '21, '22, '23, '24
PC member.
ETAPS '24
Artifact Evaluation Committee.
ABZ '23
PC member.
Tutorial@ABZ'23
Teaching Alloy with Alloy4Fun, organizer and speaker.
ICT4S'22
OC member (web and virtualization).
QRARSAC'21
PC member.
Tutorial@IROS'21
Improving the software quality of ROS applications with HAROS, organizer and speaker.
Tutorial@FM'19
Formal software design with Alloy and Electrum, organizer and speak.

TEACHING

Computing Theory (TC)
BSc, Fall '21, Spring '22 - '25 (L.EIC@FEUP)
Programming Fundamentals (FP)
BSc, Fall '20 - '24 (L.EIC+MIEIC@FEUP)
Introduction to Programming (IPROG)
MSc, Fall '24 (MM@FEUP)
Formal Methods for Critical Systems (MFS)
MSc, Spring '22 - '24 (M.EIC@FEUP)
Discrete Mathematics (MD)
BSc, Fall '23 (L.EIC@FEUP)
Software Design and Testing Laboratory (LDTS)
BSc, Fall '22 (L.EIC@FEUP)
Operating Systems (SO)
BSc, Spring '21 (MIEIC@FEUP)
Formal Methods in Software Engineering (MFES)
MSc, Fall '20 (MIEIC@FEUP)
Program Calculation (CP)
BSc, Spring '20 (MIEI@UM)
Specification and Modelling (EM)
MSc, Fall '15, '18 - '19 (MIEI+MCC@UM)
Computer Labs I (LI1)
BSc, Fall '09, '11 - '12, '15 - '17, '19 (MIEI@UM)
Imperative Programming (PI)
BSc, Spring '18 (MIEI@UM), '19 (MIEI+LCC+MIEFis@UM)
Functional Programming (PF)
BSc, Fall '16 (LCC+MIEFis@UM), '17 (MIEI@UM)
Applied Informatics (LAD)
BSc, Spring '17 (LLA@UM)
Software Development Labs (LDS)
BSc, Fall '13 (LEI@IPP)
Checkout the LI1@UM Hall of Fame with the best student projects from 2013 to 2020.