Alcino Cunha
I’m an Associate Professor with habilitation at the Department of Informatics of University of Minho. I’m also a member (and currently co-coordinator) of the High-Assurance Software Laboratory, a research center of University of Minho and of the INESC TEC associate laboratory.
Research
My research aims to make formal software design more accessible for all software engineers. Together with colleagues at INESC TEC and ONERA, we developed the new version 6 of the popular Alloy formal specification framework, and also Alloy4Fun, a web application for sharing and learning Alloy. You can find our free online book about Alloy here. In the past I also worked on formal analysis techniques for robotic software developed with ROS, namely the HAROS framework, and on model repair and (bidirectional) transformation, namely the Echo framework .
News
| Jul 2025 | I’ll be a PC member of Formalize 2026. The deadline for submitting a paper is 23 Oct 2025. |
| Apr 2025 | I’m a PC member of SEFM 2025. Please consider submitting a paper. |
| Feb 2025 | The new version of our free online book about Alloy is available here. |
| Jan 2025 | Two papers accepted at Formalize 2025: Verifying Multiple TLA+ Configurations with Blast and Specifying Distributed Hash Tables with Allen Temporal Logic. |
| Nov 2024 | The recording of my talk at at Lambda World is available here. |
| Sep 2024 | I’m a PC member of ABZ 2025. Please consider submitting a paper. |
| Jul 2024 | I will give at talk entitled Designing Software with Complex Configurations at Lambda World. |
| Jun 2024 | We had a paper accepted at FM 2024 about generating Alloy repair hints based on historical data. |
| Jan 2024 | I gave a tutorial about Teaching Alloy with Alloy4Fun at the FMTea tutorial series. The recording of this tutorial is available here. |
Older news can be found here.
Teaching
I currently teach in the following courses at University of Minho:
- Formal Methods in Software Engineering (MSc)
- Formal Verification (MSc)
- Algorithmic Problem Solving Lab (BSc)
- Algorithms and Complexity (BSc)
- Imperative Programming (BSc)
Projects
Past projects:
- SpecRep: Constraint-based Specification Repair
- DigiLightRail: Verification of Railway Network Models (consultancy for EFACEC)
- SAFER: Safety Verification for Robotic Software (principal investigator)
- TRUST: Trustworthy Software Design with Alloy (principal investigator)
- LightKone: Lightweight Computations for Networks at the Edge
- COST IC1405: Reversible computation - extending horizons of computing
- FATBIT: Foundations, Applications and Tools for Bidirectional Transformation (principal investigator)
- PTCRISync: An ORCID based synchronisation framework for the Portuguese CRIS ecosystem
- PURe: Program Understanding and Re-engineering: Calculi and Applications
- EVOLVE: Evolutionary validation, verification and certification
Publications
Some selected publications:
- Alcino Cunha: Designing Software with Complex Configurations. arXiv:2407.13633, July 2024. A report describing my habilitation lecture. I also gave a similar talk at Lambda World. The recording of that talk is available here.
- Alcino Cunha, Nuno Macedo, José Creissac Campos, Iara Margolis, Emanuel Sousa: Assessing the impact of hints in learning formal specification. In proceedings of the Software Engineering Education and Training track of the 46th International Conference on Software Engineering (ICSE SEET’24), pages 151-161. ACM, 2024.
- Pedro Silva, José N. Oliveira, Nuno Macedo, Alcino Cunha: Quantitative Relational Modelling with QAlloy. In proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE’22), pages 885-896. ACM, 2022.
- Nuno Macedo, Julien Brunel, David Chemouil, Alcino Cunha: Pardinus: A Temporal Relational Model Finder. Journal of Automated Reasoning 66: 861-904. Springer, 2022.
- Nuno Macedo, Alcino Cunha, José Pereira, Renato Carvalho, Ricardo Silva, Ana C. R. Paiva, Miguel Sozinho Ramalho, Daniel Castro Silva: Experiences on teaching Alloy with an automated assessment platform. Science of Computer Programming 211: 102690. Elsevier, 2021.
- Renato Carvalho, Alcino Cunha, Nuno Macedo, André Santos: Verification of system-wide safety properties of ROS applications. In proceedings of the 2020 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS’20), pages 7249-7254. IEEE, 2020.
- Alcino Cunha, Nuno Macedo: Validating the Hybrid ERTMS/ETCS Level 3 concept with Electrum. International Journal on Software Tools for Technology Transfer 22(3): 281-296. Springer, 2020.
- Nuno Macedo, Jorge Tiago, Alcino Cunha: A Feature-based Classification of Model Repair Approaches. IEEE Transactions on Software Engineering 43(7): 615-640. IEEE, 2017.
- Nuno Macedo, Julien Brunel, David Chemouil, Alcino Cunha, Denis Kuperberg: Lightweight specification and analysis of dynamic systems with rich configurations. In proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE’16), pages 373-383. ACM, 2016.
- Alcino Cunha, Ana Gabriela Garis, Daniel Riesco: Translating between Alloy specifications and UML class diagrams annotated with OCL. Software and System Modeling 14(1): 5-25. Springer, 2015.
- Nuno Macedo, Alcino Cunha: Implementing QVT-R Bidirectional Model Transformations Using Alloy. In proceedings of the 16th International Conference on Fundamental Approaches to Software Engineering (FASE’13), volume 7793 of LNCS, pages 297-311. Springer, 2013.
My full publication list can be found at DBLP or Scholar.
Students
- Manuel Barros (PhD, w/ Eunsuk Kang and José Orlando Pereira)
Alumni:
- Chong Liu (PhD, w/ Nuno Macedo, 2022). She is now at East China Jiaotong University.
- André Santos (PhD, w/ Nuno Macedo, 2021). He is now at Vortex CoLab.
- Ana Garis (PhD, w/ Daniel Riesco, 2015). She is now at Universidade Nacional de San Luis.
- Nuno Macedo (PhD, w/ José Nuno Oliveira, 2014). He is now at University of Porto.
- Hugo Pacheco (PhD, 2012). He is now at University of Porto.
The full list of my alumni can be found here.
Service
- ABZ: 2025 (PC), 2024 (PC)
- SEFM: 2025 (PC), 2024 (PC), 2023 (PC)
- QRARSAC: 2023 (Co-chair), 2021 (Co-chair)
- Bx: 2021 (PC), 2018 (PC), 2015 (Co-chair), 2012 (PC)
Older service can be found here.
Personal
I love traveling, photography (Flickr, Instagram, 500px), and cycling (Strava). My wife Rosa Cabecinhas is an Associate Professor with Habilitation at the Institute of Social Sciences at University of Minho.