About
I am a professor at the Computer Science Department, Universidade do Minho, and a research coordinator at the High Assurance Software Laboratory (HASLab) of INESCTEC. I've served as Deputy Head of the Department from June 2024 to May 2026.
I hold a PhD from École Polytechnique on Interaction Nets and the Geometry of Interaction. My research since then has focused on deductive program verification — currently on distributed algorithm verification and safe AI.
Most recent work:
The TLA+ Trifecta Walks into a Bar, the Bartender Asks Why3?
With I. Chirica, M. Pereira. In ISoLA 2026 — 13th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (Kos, Greece, 24–28 October). LNCS, Springer, pp. 96–116. Springer →
Verified Tensor Operators for Safety-Critical ML
With J. Machado, R. Silva, L. Correnson, J. Galego, E. Jenn, H. D. Macedo, J. Souyris. A formally verified workflow (abstract WhyML spec to extracted C code) for ONNX tensor operators, demonstrated on seven operators and a complete logistic regression network. In SAIV 2026 — 9th Symposium on AI Verification (Lisbon, 24–25 July). LNCS, Springer. Springer →
Rigorous Software Development, 2nd ed.
Co-authored with J. B. Almeida, M. J. Frade, S. M. de Sousa. Revised and expanded, with new tools including Frama-C/WP for verifying C programs with ACSL. Springer Undergraduate Topics in Computer Science.
Why3-do
A WhyML library for auto-active verification of distributed systems. The ESOP 2022 paper introduced handler-based models; a follow-up in Science of Computer Programming (2026) generalises to state machine specifications, adds refinement support, and includes Paxos as a case study.
Teaching
-
2026/27
Métodos Formais em Engenharia de Software Mestrado em Engenharia Informática
An introduction to Formal Methods covering logic, automated reasoning, structural and behavioural modelling with Alloy, and deductive verification with Why3. Course page
-
2026/27
Algoritmos e Complexidade Licenciatura em Engenharia Informática
An undergraduate course on algorithms covering core and advanced topics of AL–CS2013 in the IEEE/ACM curricula. Course page
-
2025/26
Verificação Formal Mestrado em Engenharia Informática
An elective on formal verification covering SAT/SMT tools, the Coq proof assistant, deductive verification with Why3 and Frama-C, software model checking, and verification of distributed algorithms. Course page
-
2025/26
Dados e Computação Licenciatura em Engenharia Física
A first-cycle course on data and computation for engineering physics students. Course page
Books & Edited Volumes
- Rigorous Software Development: An Introduction to Program Verification Springer →
- A Tribute to José Manuel Valença Sciencedirect →
- LerNet Summer School — Revised, Selected Papers Springer →
Research Projects
-
BringTrust
2025–2028
Strengthening CI/CD Pipeline Cybersecurity and Safeguarding Intellectual Property
Industry co-promotion project involving Scalabit, Universidade do Algarve, and HASLab/INESC TEC. COMPETE2030/FEDER funded.
-
SafeIaC
2025–2027
Reliable Analysis and Automated Repair for Infrastructure as Code
FCT-funded project on analysis and automated repair for Infrastructure as Code. Project page
-
VeriFixer
2025–2026
Automated Repair for Verification-Aware Programming Languages
FCT-funded (PEX). Project page
-
DReason
2026
Leveraging Deductive Verification to Distributed Systems
FCT-funded (PEX).
-
SAFER
2018–2021
Safety Verification for Robotic Software
Applications of formal methods in the context of robotics systems. FCT-funded. Project page
-
REASSURE
2018–2021
Runtime Verification for Reliable Real-Time Embedded Software
A framework extending runtime monitoring with safety and security guarantees, with automatic monitor generation and deployment. FCT-funded. Project page
-
AVIACC
2012–2015
Analysis and Verification of Critical Concurrent Programs
The interplay between deductive methods and model checking for safety-critical systems. FCT-funded. Project page
Research Students
Current
- Miguel Liquito MSc — deductive verification of ephemeral trust for secure CI/CD runners GitHub
- Carolina de Passos Sá MSc — formal modelling and verified security analysis of GitHub Actions workflows GitHub
- Ion Chirica PhD, NOVA FCT — auto-active verification of distributed systems (co-supervised with Mário Pereira)
- João Costa Marques Machado MSc — runtime monitoring and adaptive safety assurance for ONNX models (co-supervised with Hugo Macedo)
- Ricardo Moreira da Silva MSc — formal safety guarantees for ONNX models in safety-critical applications (co-supervised with Hugo Macedo) GitHub
- Carlos Alberto Ribeiro MSc — an algebra for algorithmic complexity (co-supervised with José Nuno Oliveira)
Former
- André de Matos Pedro Professor Auxiliar, Universidade da Beira Interior (Portugal)
- Cláudio Belo Lourenço Principal Engineer (Programming Languages), Huawei Technologies R&D (UK)
- Daniela da Cruz Director of Engineering, Datadog
- Iago Abal Senior/Lead Software Engineer (Program Analysis), Semgrep (USA)
- João Carlos Pereira PhD student, Programming Methodology Group, ETH Zürich
- João Martins Frameworks and Software Architecture Leader, EFACEC (Portugal)
- José Miguel Faria Director, Safe Perspective Ltd (UK)
- Rovedy Silva Researcher, Instituto de Aeronáutica e Espaço (IAE, Brazil)
- Vítor Miraldo Software Engineer, Converge (UK)
Elsewhere
Departamento de Informática, Universidade do Minho, Campus de Gualtar, 4710-057 Braga, Portugal