SELECTED PUBLICATIONS
- P. Silva, J. N. Oliveira, N. Macedo and A. Cunha. Quantitative relational modelling with QAlloy. 21st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE 2022). ACM, 2022.
- R. Carvalho, A. Cunha, N. Macedo and A. Santos. Verification of system-wide safety properties of ROS applications. 2020 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS 2020). IEEE/RSJ, 2020.
- N. Macedo, T. Jorge and A. Cunha. A feature-based classification of model repair approaches. IEEE Transactions on Software Engineering, 2017.
- N. Macedo, J. Brunel, D. Chemouil, A. Cunha and D. Kuperberg. Lightweight specification and analysis of dynamic systems with rich configurations. 24th ACM SIGSOFT International Symposium on the Foundations of Software Engineering (FSE 2016). ACM, 2016.
- N. Macedo and A. Cunha. Least-change bidirectional model transformation with QVT-R and ATL. Software and Systems Modeling, 2016.
The full list of publications, and associated resources, can be consulted
here (or more easily at
DBLP or
Google Scholar).
CURRENT PROJECTS
- SpecRep
- Constraint-based Specification Repair, an FCT exploratory project that aims to develop techniques to support the automatic repair of faulty specifications.
PAST PROJECTS
- 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
- Co-supervision of the PhD thesis on "High-level quantitative relational model finding".
- Gédsimon Pereira
- Supervision of the MSc thesis on "Stateful security testing of web APIs".
- Valentina Wu
- Co-supervision of the MSc thesis on "Automated repair for verification-aware programming languages".
- Rui Gonçalves
- Co-supervision of the MSc thesis on "Security verification for trustworthy software design".
- David Guedes
- Co-supervision of the MSc thesis on "Security-aware specifications for web APIs".
PAST STUDENTS
- 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
- Co-supervision of the PhD thesis on "Lightweight trustworthy high-level software design".
- André Santos
- Co-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
- ETAPS '24
- Artifact Evaluation Committee.
- ABZ '23
- PC member.
- Tutorial@ABZ'23
- Teaching Alloy with Alloy4Fun, organizer and speaker.
- SBLP '22,'23
- PC member.
- IRC '21, '22, '23
- PC member.
- 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
- Formal Methods for Critical Systems (MFS)
- MSc, Spring '22 - '24 (M.EIC@FEUP)
- Computing Theory (TC)
- BSc, Fall '21, Spring '22 - '24 (L.EIC@FEUP)
- Programming Fundamentals (FP)
- BSc, Fall '20 - '23 (L.EIC+MIEIC@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.