About

João F. Ferreira is an associate professor at IST, University of Lisbon, and a researcher at INESC-ID. He co-leads the Software Reliability Lab. He coordinates the Automated Reasoning and Software Reliability area at INESC-ID. His work spans from empirical software engineering methods that can inform practitioners and direct future research, to formal methods that can verify the absence of certain types of bugs. For more details, see selected publications.

Interests

  • Software Reliability
  • Software Verification
  • Formal Methods applied to Software Engineering
  • Empirical Software Engineering

Education

  • PhD in Computer Science

    University of Nottingham, UK

  • BSc in Mathematics and Computer Science

    Minho University, Portugal

Recent Publications

View all the publications

Quickly discover relevant content by filtering publications.
Robert Thompson, Nuno Saavedra, Pedro Carrott, Kevin Fisher, Alex Sanchez-Stern, Yuriy Brun, João F. Ferreira, Sorin Lerner, Emily First (2025). Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification. In ICSE 2025. CORE A* conference.
🏆 ACM SIGSOFT Distinguished Paper award.

PDF Code Dataset

Nuno Saavedra, João F. Ferreira, afm (2025). InfraFix: Technology-Agnostic Repair of Infrastructure as Code. In ISSTA 2025, Tool Demonstrations Track. CORE A conference.

PDF Code Video

Sogol Masoumzadeh, Nuno Saavedra, Rungroj Maipradit, Lili Wei, João F. Ferreira, Dániel Varró, Shane McIntosh (2025). Do Experts Agree About Smelly Infrastructure?. In TSE 2025. Q1 journal.

PDF

David Ferreira, Alexandra Mendes, João F. Ferreira, Carolina Carreira (2025). Contract Usage and Evolution in Android Mobile Applications. In ECOOP 2025. CORE A conference.

PDF Code

Pedro Carrott, Nuno Saavedra, Robert Thompson, Sorin Lerner, João F. Ferreira, Emily First (2024). CoqPyt: Proof Navigation in Python in the Era of LLMs. In FSE 2024, Demonstrations Track. CORE A* conference.

PDF Code Video

See all publications

Selected Projects

View all the projects

Smartbugs

Executional framework for running analysis tools on smart contracts.

Password Security

Tools and methods to improve password security.

Interactive Narratives

Tools and methods for computer-generated narratives.

FM Education

Tools, methods, and resources that support teaching formal methods.

Recent Posts

View all the posts

SmartBugs: An Execution Framework for Automated Analysis of Smart Contracts

SmartBugs is a new execution framework that simplifies the execution of automated analysis tools on datasets of Solidity smart contracts. SmartBugs currently supports 10 tools. It has a simple plugin system to easily add new analysis tools, based on Docker images. It supports parallel execution of the tools to speed up the execution time. It also normalizes the output that tools produce to facilitate experiments. SmartBugs was developed in the context of an empirical review of automated analysis tools on 47,587 Ethereum smart contracts.
Mar 5, 2020 4 min read
SmartBugs: An Execution Framework for Automated Analysis of Smart Contracts

An Improved Proof of the Handshaking Lemma

In 2009, I posted a calculational proof of the handshaking lemma, a well-known elementary result on undirected graphs. I was very pleased about my proof because the amount of guessing involved was very small (especially when compared with conventional proofs). However, one of the steps was too complicated and I did not know how to improve it. In June, Jeremy Weissmann read my proof and he proposed a different development. His argument was well structured, but it wasn’t as goal-oriented as I’d hoped for.
Sep 20, 2011 6 min read Mathematics
An Improved Proof of the Handshaking Lemma

Principles and Applications of APS

I am currently in Salamanca (Spain), attending the conference Tools for Teaching Logic III. My talk was on teaching logic through algorithmic problem solving and it went quite well, I think. In particular, it seems that the audience enjoyed the examples that I have used and the teaching scenarios that I have shown. As a result, I have promised that I would upload my PhD thesis into this website. Since the thesis can also be useful for other people, I have decided to write a new blog post.
Jun 2, 2011 2 min read Algorithms, Mathematics

Probabilities in Proofreading

Suppose you write a program and you send the source code to two of your friends, ${\cal A}$ and ${\cal B}$. Your two friends read the code and when they finish, $A$ errors are detected by ${\cal A}$, $B$ errors are detected by ${\cal B}$, and $C$ errors are detected by both. So, in total, $A+B−C$ errors are detected and can now be eliminated. We wish to estimate the number of errors that remain unnoticed and uncorrected.
Sep 14, 2009 2 min read Mathematics

Multiples in the Fibonacci Series

I found the following problem on K. Rustan M. Leino’s puzzles page: [Carroll Morgan told me this puzzle.] Prove that for any positive K, every Kth number in the Fibonacci sequence is a multiple of the Kth number in the Fibonacci sequence. More formally, for any natural number n, let F(n) denote Fibonacci number n. That is, F(0) = 0, F(1) = 1, and F(n+2) = F(n+1) + F(n).
May 9, 2008 2 min read Mathematics
See all posts

Contact