Ph.D. candidate at FEUP affiliated with CMU

Building verification tools people actually want to use.

I work at the intersection of formal methods, software engineering, and hardware verification. My current research focuses on improving the usability of verification-aware languages, with a strong emphasis on Dafny, alongside work on VeriFixer and adjacent verification ecosystems such as Verus. I am doing my Ph.D. under the supervision of Alexandra Mendes and co-supervision of Ruben Martins.

Explore projects Get in touch

Research Usability of verification-aware languages, Dafny, proof support, and AI-assisted verification.

Industry Four years in ASIC verification, with MIPI camera controllers and ISO 26262 experience.

Teaching Guest assistant in Functional Programming, Logic Programming, Python, and Computing Systems.

Featured work

Research

Dafny usability research

I investigate how AI and better tool feedback can improve the experience of writing and proving programs in Dafny. The goal is not only stronger automation, but clearer proof workflows and more approachable formal development.

Project

VeriFixer

Research on automated repair for verification-aware languages, starting with Dafny. The project aims to reduce the gap between verification errors and actionable fixes.

Exploration

Verus and verification ergonomics

Verus is a useful comparison point for thinking about how verification can integrate with systems programming. It fits naturally into a broader story about making formal methods more usable and more widely adopted.

Industry

MIPI camera controllers

As verification lead engineer, I built constrained-random environments, temporal assertions, and formal checks for CSI-2 camera controllers in automotive-oriented contexts.

Experience

Ph.D. Candidate, FEUP affiliated CMU

Sep 2024 - ongoing · Porto, Portugal

Grant under the CMU Portugal Affiliated Ph.D. Program.
Researching the usability of formal tools, with a focus on Dafny.
Member of the VeriFixer project.

Guest Assistant, FEUP

Sep 2024 - ongoing · Porto, Portugal

Lecturing Functional and Logic Programming, Fundamentals of Programming in Python, and Computing Systems.

ASIC Digital Design Staff Engineer, Synopsys

Aug 2021 - Sep 2024 · Porto, Portugal

Functional verification for digital IP, especially automotive products.
ISO 26262 certification for automotive safety products.
Applied formal verification with VCFormal and wrote assertions from specifications.

Researcher, INESC TEC

Oct 2020 - Aug 2021 · Porto, Portugal

Integrated the European research project TRUST AI.
Held two research scholarships during this period.

Education and awards

Education

Integrated Masters in Electrical and Computer Engineering

FEUP · 2016 - 2021

Graduated with 19/20.
Minor in Telecommunications.
Specialization in Micro-electronics.

Erasmus exchange master student

TUM · 2019 - 2020

One semester at Technische Universität München.

Recognition

Merit awards

Merit scholarship awards in 2016-2017 and 2017-2018.
Incentivo 2018 award as one of the top 20 first-year students at FEUP.

Leadership and collaboration

Team leader on a 40-person university project.
Worked on wireless sensor and SDR-based communication systems.

Selected publications

Leveraging Large Language Models to Boost Dafny's Developers Productivity FormaliSE 2024 · Álvaro Silva, Alexandra Mendes, and João F. Ferreira

Can Large Language Models Help Students Prove Software Correctness? An Experimental Study with Dafny arXiv, accepted in SEFM 2025 · Carolina Carreira, Álvaro Silva, Alexandre Abreu, and Alexandra Mendes

Inferring Multiple Helper Dafny Assertions with LLMs arXiv, under review 2025 · Álvaro Silva, Alexandra Mendes, and Ruben Martins

Using Dimensional Aware Genetic Programming to find interpretable Dispatching Rules for the Job Shop Scheduling Problem Master's thesis · Faculty of Engineering of the University of Porto, 2021

Contact

Let’s talk about verification, research, and practical tooling.

If you want to discuss Dafny, Verus, program repair, hardware verification, or research collaborations, use one of the links below.

Email LinkedIn GitHub GitLab ORCID