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 research is on mathematical approaches to software quality, with emphasis on program construction and verification. For more details, see selected publications.

Interests

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

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.
Steve Dunne, João F. Ferreira, Alexandra Mendes, Campbell Ritchie, Bill Stoddart, Frank Zeyda (2022). bGSL: An Imperative Language for Specification and Refinement of Backtracking Programs. In JLAMP.

PDF DOI

Nuno Saavedra, João F. Ferreira (2022). GLITCH: Automated Polyglot Security Smell Detection in Infrastructure as Code. In ASE 2022. Awarded: Artifact Evaluation Award (Reusable)

PDF Dataset

Ricardo Pereira, João F. Ferreira, Alexandra Mendes, Rui Abreu (2022). Extending EcoAndroid with Automated Detection of Resource Leaks. 9th IEEE/ACM International Conference on Mobile Software Engineering and Systems 2022 (MobileSoft 2022), co-located with ICSE 2022.

PDF

Miguel Grilo, João Campos, João F. Ferreira, José Bacelar Almeida, Alexandra Mendes (2022). Verified password generation from password composition policies. In iFM 2022. Invited to ACM Formal Aspects of Computing special issue on iFM 2022

PDF Code

Miguel Trinca, João F. Ferreira, Rui Abreu (2022). A Preliminary Study on Generating Well-Formed Q# Quantum Programs for Fuzz Testing. In AIST 2022.

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