I'm an assistant professor at the Department of Informatics of the University of Minho, Portugal, and a 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. Checkout the answer to the ABZ18 call for case study contributions to have an idea of the features of this new version. I'm also the maintainer of Alloy4Fun, an automated assessment platform for learning Alloy.
In a concrete application domain, I've been tailoring such techniques for the robotics domain to promote the development of dependable robotics software. I've also applied such techniques in consultancy projects, like the PTCRIS project commissioned by the Portuguese Foundation for Science and Technology.
Contacts
Departamento de Informática
Universidade do Minho, Edifício 7,
Campus de Gualtar,
4710-057 Braga, Portugal
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.
Constraint-based Specification Repair, an FCT exploratory project that aims to develop techniques to support the automatic repair of faulty specifications.
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.
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.
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.
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.
