Nuno Moreira Macedo

I'm an assistant professor at the Department of Informatics Engineering (DEI) of the Faculty of Engineering of the University of Porto (FEUP), Portugal, and a senior researcher at HASLab, INESC TEC's unit focused on high-assurance software development, developing, teaching and applying formal techniques for software engineering.

My main research interest lies in trustworthy software design, particularly in the application of lightweight formal methods based on model checking and model finding to software engineering. I'm one of the developers of Alloy 6 and its Analyzer, a tool to analyze software models. I've also been tailoring such techniques for the robotics domain to promote the development of dependable robotics software, and I've applied them in knowledge transfer and consultancy projects.

My teaching activities mainly focus on programming languages and formal methods for software engineering. In this context, I also maintain Alloy4Fun, a platform for teaching Alloy.

Domains

High-Assurance Software Computer Science and Engineering Robotics

Projects

NanoStima-RL1

Project NanoSTIMA will try to respond to two great challenges: going from the current macro technologies used today to micro and nano technologies, which will play a key role in the health and well-being sectors; and managing the large amounts of information that these wearable and implantable sensors will generate, integrating them with data from other sources, such as medical records, genetic data, and even social networks. The project’s research line 1 will be developed by two INESC TEC centres: C-BER and CAP. At C-BER, the goal of CAD-RL5 is to develop advanced capabilities for computer-aided detection and diagnosis (CAD). This requires research on innovative methodologies for CAD development, that will make it possible to go from ad hoc engineering approaches, driven by direct expert knowledge, to more automated approaches, driven by the intrinsic structure of data, knowledge discovery and expert supervision. Problems tackled will be generic in the sense that appropriate outcomes can be applied universally to medical imaging practices. The developed method will enable lab demonstrations of several clinical problems where the research team has relevant experience (e.g. radiology, ophthalmology and ultrasound imaging).

NanoSTIMA - Macro-to-Nano Human Sensing Technologies

SAFER

The SAFER project aimed to develop techniques and tools for ensuring the quality of robotic software developed with ROS. To facilitate the integration and adoption by the robotics community, the project focused on developing techniques that worked directly from source code and supported by automated verification tools. The main deliverable of the project was the HAROS tool for static analysis of ROS software.

View all projects

Publications

Validating multiple variants of an automotive light system with Alloy 6

Cunha, A;Macedo, N;Liu, C;

2024

INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER

Assessing the impact of hints in learning formal specification

Cunha, A;Macedo, N;Campos, JC;Margolis, I;Sousa, E;

2024

2024 ACM/IEEE 44TH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING: SOFTWARE ENGINEERING EDUCATION AND TRAINING, ICSE-SEET 2024

A relational approach to bidirectional transformation

Macedo, N;

2014

Exploring Automatic Specification Repair in Dafny Programs

Abreu, A;Macedo, N;Mendes, A;

2023

2023 38TH IEEE/ACM INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING WORKSHOPS, ASEW

View all publications

Supervised theses

Digital Twin of Reconfigurable Printed IoT Nodes using ns-3

Tiago da Silva Ribeiro

M - 2023

UP-FEUP

Centres

High-Assurance Software

At the High-Assurance Software Laboratory (HASLab), we improve practice through theory, creating and implementing software that goes beyond mere functionality: we ensure it is correct, resilient, and secure against failures and attacks. Our team of researchers, scientists, and engineers has proven expertise in software engineering, developing methods and tools to design and integrate robust software; in distributed systems, exploring distribution and replication to ensure scalability and reliability; and in information security, addressing cybersecurity challenges and improving systems with advanced, secure cryptographic protocols, thus minimising vulnerabilities. With a multidisciplinary approach supported by solid theoretical principles, we develop innovative solutions for critical software, secure cloud infrastructures, and privacy-aware big data management, driving scientific advancement, innovation, and high-level consultancy. In addition, we complement our core expertise with work in human-computer interaction, programming languages, computational mathematics, and quantum computing - because we believe the future of trustworthy software is built on knowledge and innovation.