João F. Ferreira

Computer Scientist

IST, University of Lisbon

INESC-ID, Lisboa


João F. Ferreira is an assistant professor at IST, University of Lisbon, and a researcher at INESC-ID. His research is on mathematical approaches to software quality, with emphasis on program construction and verification. For more details, see selected publications.


  • Software Reliability
  • Software Verification
  • Formal Methods applied to Software Engineering
  • Interactive Storytelling


  • PhD in Computer Science

    University of Nottingham, UK

  • BSc in Mathematics and Computer Science

    Minho University, Portugal

Selected Projects

View all the projects


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 …

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 …

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 …

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 …

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 …