João F. Ferreira

João F. Ferreira

Computer Scientist

IST, University of Lisbon

INESC-ID, Lisboa

About

João F. Ferreira is an associate professor at IST, University of Lisbon, and a researcher 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 (2024). Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification. In ICSE 2025. CORE A* conference.

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

David Ferreira, Alexandra Mendes, João F. Ferreira (2024). How are Contracts Used in Android Mobile Applications?. In ICSE 2024, Poster Paper. CORE A* conference.

PDF

Monika di Angelo, Thomas Durieux, João F. Ferreira, Gernot Salzer (2024). Evolution of automated weakness detection in Ethereum bytecode: a comprehensive study. In EMSE, 29(2), pp. 1-44. Q1 Journal.

PDF Code Project DOI

Álvaro Silva, Alexandra Mendes, João F. Ferreira (2024). Leveraging Large Language Models to Boost Dafny's Developers Productivity. In FormaliSE 2024, co-located with ICSE 2024.

PDF

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