João F. Ferreira

@ulisboa.pt

INESC-ID & Instituto Superior Técnico, University of Lisbon



                        Download Compact PDF  

https://researchid.co/jff

RESEARCH INTERESTS

My research interests include software reliability, software verification, and formal methods applied to software engineering. I am also interested in interactive storytelling.

62

Scopus Publications

2099

Scholar Citations

20

Scholar h-index

44

Scholar i10-index

Scopus Publications

  • Are Users More Willing to Use Formally Verified Password Managers?
    Carolina Carreira, João F. Ferreira, Alexandra Mendes, Nicolas Christin
    Lecture Notes in Computer Science, 2026
  • Contract Usage and Evolution in Android Mobile Applications
    David R. Ferreira, A. Mendes, João F. Ferreira, Caroline Carreira
    Leibniz International Proceedings in Informatics Lipics, 2025
  • Do Experts Agree About Smelly Infrastructure?
    Sogol Masoumzadeh, Nuno Saavedra, Rungroj Maipradit, Lili Wei, João F. Ferreira, et al.
    IEEE Transactions on Software Engineering, 2025
    —Code smells are anti-patterns that violate code un-derstandability, re-usability, changeability, and maintainability. It is important to identify code smells and locate them in the code. For this purpose, automated detection of code smells is a sought-after feature for development tools; however, the design and evaluation of such tools depends on the quality of oracle datasets. The typical approach for creating an oracle dataset involves multiple developers independently inspecting and annotating code examples for their existing code smells. Since multiple inspectors cast votes about each code example, it is possible for the inspectors to disagree about the presence of smells. Such disagreements introduce ambiguity into how smells should be interpreted. Prior work has studied developer perceptions of code smells in traditional source code; however, smells in Infrastructure-as-Code (IaC) have not been investigated. To understand the real-world impact of disagreements among developers and their perceptions of IaC code smells, we conduct an empirical study on the oracle dataset of GLITCH—a state-of-the-art detection tool for security code smells in IaC. We analyze GLITCH’s oracle dataset for code smell issues, their types, and individual annotations of the inspectors. Furthermore, we investigate possible confounding factors associated with the incidences of developer misaligned perceptions of IaC code smells. Finally, we triangulate developer perceptions of code smells in traditional source code with our results on IaC. Our study reveals that unlike developer perceptions of smells in traditional source code, their perceptions of smells in IaC are more substantially impacted by subjective interpretation of smell types and their co-occurrence relationships. For instance, the interpretation of admins by default, empty passwords, and hard-coded secrets varies considerably among raters and are more susceptible to misidentification than other IaC code smells. Consequently, the manual identification of IaC code smells involves annotation disagreements among developers—46.3% of studied
  • Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification
    Proceedings International Conference on Software Engineering, 2025
  • CoqPyt: Proof Navigation in Python in the Era of LLMs
    Pedro Carrott, Nuno Saavedra, Kyle Thompson, Sorin Lerner, João F. Ferreira, et al.
    Fse Companion Companion Proceedings of the 32nd ACM International Conference on the Foundations of Software Engineering, 2024
    Proof assistants enable users to develop machine-checked proofs regarding software-related properties. Unfortunately, the interactive nature of these proof assistants imposes most of the proof burden on the user, making formal verification a complex, and time-consuming endeavor. Recent automation techniques based on neural methods address this issue, but require good programmatic support for collecting data and interacting with proof assistants. This paper presents CoqPyt, a Python tool for interacting with the Coq proof assistant. CoqPyt improves on other Coq-related tools by providing novel features, such as the extraction of rich premise data. We expect our work to aid development of tools and techniques, especially LLM-based, designed for proof synthesis and repair. A video describing and demonstrating CoqPyt is available at: https://youtu.be/fk74o0rePM8.
  • Leveraging Large Language Models to Boost Dafny's Developers Productivity
    Álvaro F. Silva, Alexandra Mendes, João F. Ferreira
    Proceedings 2024 IEEE ACM 12th International Conference on Formal Methods in Software Engineering Formalise 2024, 2024
    This research idea paper proposes leveraging Large Language Models (LLMs) to enhance the productivity of Dafny developers. Although the use of verification-aware languages, such as Dafny, has increased considerably in the last decade, these are still not widely adopted. Often the cost of using such languages is too high, due to the level of expertise required from the developers and challenges that they often face when trying to prove a program correct. Even though Dafny automates a lot of the verification process, sometimes there are steps that are too complex for Dafny to perform on its own. One such case is that of missing lemmas, i.e. Dafny is unable to prove a result without being given further help in the form of a theorem that can assist it in the proof of the step.In this paper, we describe preliminary work on using LLMs to assist developers by generating suggestions for relevant lemmas that Dafny is unable to discover and use. Moreover, for the lemmas that cannot be proved automatically, we attempt to provide accompanying calculational proofs. We also discuss ideas for future work by describing a research agenda on using LLMs to increase the adoption of verification-aware languages in general, by increasing developers productivity and by reducing the level of expertise required for crafting formal specifications and proving program properties.CCS CONCEPTS• Software and its engineering → Software notations and tools; Software verification and validation.
  • DifFuzzAR: automatic repair of timing side-channel vulnerabilities via refactoring
    Rui Lima, João F. Ferreira, Alexandra Mendes, Carolina Carreira
    Automated Software Engineering, 2024
    Vulnerability detection and repair is a demanding and expensive part of the software development process. As such, there has been an effort to develop new and better ways to automatically detect and repair vulnerabilities. DifFuzz is a state-of-the-art tool for automatic detection of timing side-channel vulnerabilities, a type of vulnerability that is particularly difficult to detect and correct. Despite recent progress made with tools such as DifFuzz, work on tools capable of automatically repairing timing side-channel vulnerabilities is scarce. In this paper, we propose DifFuzzAR, a tool for automatic repair of timing side-channel vulnerabilities in Java code. The tool works in conjunction with DifFuzz and it is able to repair 56% of the vulnerabilities identified in DifFuzz’s dataset. The results show that the tool can automatically correct timing side-channel vulnerabilities, being more effective with those that are control-flow based. In addition, the results of a user study show that users generally trust the refactorings produced by DifFuzzAR and that they see value in such a tool, in particular for more critical code.
  • How are Contracts Used in Android Mobile Applications?
    David R. Ferreira, Alexandra Mendes, Joao F. Ferreira
    Proceedings International Conference on Software Engineering, 2024
    Formal contracts and assertions are effective methods to enhance software quality by enforcing preconditions, postconditions, and invariants. However, the adoption and impact of contracts in the context of mobile application development, particularly of Android applications, remain unexplored. We present the first large-scale empirical study on the presence and use of contracts in Android applications, written in Java or Kotlin. We consider 2,390 applications and five categories of contract elements: conditional runtime exceptions, APIs, annotations, assertions, and other. We show that most contracts are annotation-based and are concentrated in a small number of applications.
  • Evolution of automated weakness detection in Ethereum bytecode: a comprehensive study
    Monika di Angelo, Thomas Durieux, João F. Ferreira, Gernot Salzer
    Empirical Software Engineering, 2024
    Blockchain programs (also known as smart contracts) manage valuable assets like cryptocurrencies and tokens, and implement protocols in domains like decentralized finance (DeFi) and supply-chain management. These types of applications require a high level of security that is hard to achieve due to the transparency of public blockchains. Numerous tools support developers and auditors in the task of detecting weaknesses. As a young technology, blockchains and utilities evolve fast, making it challenging for tools and developers to keep up with the pace. In this work, we study the robustness of code analysis tools and the evolution of weakness detection on a dataset representing six years of blockchain activity. We focus on Ethereum as the crypto ecosystem with the largest number of developers and deployed programs. We investigate the behavior of single tools as well as the agreement of several tools addressing similar weaknesses. Our study is the first that is based on the entire body of deployed bytecode on Ethereum’s main chain. We achieve this coverage by considering bytecodes as equivalent if they share the same skeleton. The skeleton of a bytecode is obtained by omitting functionally irrelevant parts. This reduces the 48 million contracts deployed on Ethereum up to January 2022 to 248 328 contracts with distinct skeletons. For bulk execution, we utilize the open-source framework SmartBugs that facilitates the analysis of Solidity smart contracts, and enhance it to accept also bytecode as the only input. Moreover, we integrate six further tools for bytecode analysis. The execution of the 12 tools included in our study on the dataset took 30 CPU years. While the tools report a total of 1 307 486 potential weaknesses, we observe a decrease in reported weaknesses over time, as well as a degradation of tools to varying degrees.
  • Hoogle: Constants and λ-abstractions in Petri-net-based Synthesis using Symbolic Execution
    Leibniz International Proceedings in Informatics Lipics, 2023
  • SmartBugs 2.0: An Execution Framework for Weakness Detection in Ethereum Smart Contracts
    Monika di Angelo, Thomas Durieux, João F. Ferreira, Gernot Salzer
    Proceedings 2023 38th IEEE ACM International Conference on Automated Software Engineering Ase 2023, 2023
  • Polyglot Code Smell Detection for Infrastructure as Code with GLITCH
    Nuno Saavedra, João Gonçalves, Miguel Henriques, João F. Ferreira, Alexandra Mendes
    Proceedings 2023 38th IEEE ACM International Conference on Automated Software Engineering Ase 2023, 2023
  • bGSL: An imperative language for specification and refinement of backtracking programs
    Steve Dunne, João F. Ferreira, Alexandra Mendes, Campbell Ritchie, Bill Stoddart, et al.
    Journal of Logical and Algebraic Methods in Programming, 2023
  • Integrating an academic management system with blockchain: A case study
    Sérgio Guerreiro, João F. Ferreira, Tiago Fonseca, Miguel Correia
    Blockchain Research and Applications, 2022
  • GLITCH: Automated Polyglot Security Smell Detection in Infrastructure as Code
    Nuno Saavedra, João F. Ferreira
    ACM International Conference Proceeding Series, 2022
  • A Preliminary Study on Generating Well-Formed Q# Quantum Programs for Fuzz Testing
    Miguel Trinca, Joao F. Ferreira, Rui Abreu
    Proceedings 2022 IEEE 14th International Conference on Software Testing Verification and Validation Workshops Icstw 2022, 2022
  • Message from the RSDA 2022 Workshop Chairs: ISSREW 2022
    Raffaele Della Corte, Marta Catillo, Joao F. Ferreira, Guanpeng Li
    Proceedings 2022 IEEE International Symposium on Software Reliability Engineering Workshops Issrew 2022, 2022
  • Extending EcoAndroid with Automated Detection of Resource Leaks
    Ricardo B. Pereira, J. Ferreira, A. Mendes, Rui Abreu
    Proceedings 9th IEEE ACM International Conference on Mobile Software Engineering and Systems Mobilesoft 2022, 2022
  • Verified Password Generation from Password Composition Policies
    Miguel Grilo, João Campos, João F. Ferreira, José Bacelar Almeida, Alexandra Mendes
    Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics, 2022
  • Exploring usable security to improve the impact of formal verification: A research agenda
    Carolina Carreira, João F. Ferreira, Alexandra Mendes, Nicolas Christin
    Electronic Proceedings in Theoretical Computer Science Eptcs, 2021
  • Automated narrative planning model extension
    Julie Porteous, João F. Ferreira, Alan Lindsay, Marc Cavazza
    Autonomous Agents and Multi Agent Systems, 2021
  • Preface
    Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics, 2021
  • Automatic Repair of Java Code with Timing Side-Channel Vulnerabilities
    Rui Lima, Joao F. Ferreira, Alexandra Mendes
    Proceedings 2021 36th IEEE ACM International Conference on Automated Software Engineering Workshops Asew 2021, 2021
  • EcoAndroid: An Android Studio Plugin for Developing Energy-Efficient Java Mobile Applications
    Ana Ribeiro, Joao F. Ferreira, Alexandra Mendes
    IEEE International Conference on Software Quality Reliability and Security Qrs, 2021
  • Message from the RSDA 2021 Workshop Chairs
    Proceedings 2021 IEEE International Symposium on Software Reliability Engineering Workshops Issrew 2021, 2021

RECENT SCHOLAR PUBLICATIONS

  • An Empirical Study of Policy as Code: Adoption, Purpose, and Maintenance
    R Opdebeeck, M Alfadel, A Rahman, Y Kashiwa, JF Ferreira, RG Kula, ...
    23rd International Conference on Mining Software Repositories (MSR2026) , 2026
    2026
    Citations: 1
  • Are Users More Willing to Use Formally Verified Password Managers?
    C Carreira, JF Ferreira, A Mendes, N Christin
    International Conference on Software Engineering and Formal Methods, 185-202 , 2025
    2025
  • Environmental Impact of CI/CD Pipelines
    N Saavedra, A Mendes, JF Ferreira
    arXiv preprint arXiv:2510.26413 , 2025
    2025
  • ProfOlaf: Semi-Automated Tool for Systematic Literature Reviews
    M Afonso, N Saavedra, B Lourenço, A Mendes, J Ferreira
    arXiv preprint arXiv:2510.26750 , 2025
    2025
  • Structuring Security: A Survey of Cybersecurity Ontologies, Semantic Log Processing, and LLMs Application
    B Lourenço, P Adão, JF Ferreira, MM Marques, C Vaz
    arXiv preprint arXiv:2510.16610 , 2025
    2025
    Citations: 4
  • InfraFix: Technology-Agnostic Repair of Infrastructure as Code
    N Saavedra, JF Ferreira, A Mendes
    Proceedings of the 34th ACM SIGSOFT International Symposium on Software … , 2025
    2025
    Citations: 4
  • The Ultimate Configuration Management Tool? Lessons from a Mixed Methods Study of Ansible's Challenges
    C Carreira, N Saavedra, A Mendes, JF Ferreira
    arXiv preprint arXiv:2504.08678 , 2025
    2025
    Citations: 4
  • A systematic review of security communication strategies: guidelines and open challenges
    C Carreira, A Mendes, JF Ferreira, N Christin
    arXiv preprint arXiv:2504.02109 , 2025
    2025
    Citations: 5
  • Do Experts Agree About Smelly Infrastructure?
    S Masoumzadeh, N Saavedra, R Maipradit, L Wei, JF Ferreira, D Varró, ...
    IEEE Transactions on Software Engineering , 2025
    2025
    Citations: 3
  • Rango: Adaptive retrieval-augmented proving for automated software verification
    K Thompson, N Saavedra, P Carrott, K Fisher, A Sanchez-Stern, Y Brun, ...
    arXiv preprint arXiv:2412.14063 , 2024
    2024
    Citations: 38
  • CoqPyt: Proof navigation in Python in the era of LLMs
    P Carrott, N Saavedra, K Thompson, S Lerner, JF Ferreira, E First
    Companion Proceedings of the 32nd ACM International Conference on the … , 2024
    2024
    Citations: 12
  • DifFuzzAR : automatic repair of timing side-channel vulnerabilities via refactoring
    R Lima, JF Ferreira, A Mendes, C Carreira
    Automated Software Engineering 31 (1), 1 , 2024
    2024
    Citations: 3
  • How are Contracts Used in Android Mobile Applications?
    DR Ferreira, A Mendes, JF Ferreira
    Proceedings of the 2024 IEEE/ACM 46th International Conference on Software … , 2024
    2024
    Citations: 1
  • Leveraging large language models to boost Dafny’s developers productivity
    ÁF Silva, A Mendes, JF Ferreira
    Proceedings of the 2024 IEEE/ACM 12th International Conference on Formal … , 2024
    2024
    Citations: 24
  • Evolution of automated weakness detection in Ethereum bytecode: a comprehensive study
    M Di Angelo, T Durieux, JF Ferreira, G Salzer
    Empirical Software Engineering 29 (2), 41 , 2024
    2024
    Citations: 32
  • Contract Usage and Evolution in Android Mobile Applications
    DR Ferreira, A Mendes, JF Ferreira
    arXiv preprint arXiv:2401.14244 , 2024
    2024
    Citations: 2
  • Polyglot code smell detection for infrastructure as code with GLITCH
    N Saavedra, J Gonçalves, M Henriques, JF Ferreira, A Mendes
    2023 38th IEEE/ACM International Conference on Automated Software … , 2023
    2023
    Citations: 15
  • Smartbugs 2.0: An execution framework for weakness detection in ethereum smart contracts
    M Di Angelo, T Durieux, JF Ferreira, G Salzer
    2023 38th IEEE/ACM International Conference on Automated Software … , 2023
    2023
    Citations: 52
  • Mufin: Improving neural repair models with back-translation
    A Silva, JF Ferreira, H Ye, M Monperrus
    arXiv preprint arXiv:2304.02301 , 2023
    2023
    Citations: 9
  • 37th European Conference on Object-Oriented Programming (ECOOP 2023)
    AD Barwell, P Hou, N Yoshida, F Zhou, J Bauwens, E Gonzalez Boix, ...
    Schloss Dagstuhl-Leibniz-Zentrum für Informatik GmbH , 2023
    2023

MOST CITED SCHOLAR PUBLICATIONS

  • Empirical review of automated analysis tools on 47,587 ethereum smart contracts
    T Durieux, JF Ferreira, R Abreu, P Cruz
    Proceedings of the ACM/IEEE 42nd International conference on software … , 2020
    2020
    Citations: 659
  • Smartbugs: A framework to analyze solidity smart contracts
    JF Ferreira, P Cruz, T Durieux, R Abreu
    Proceedings of the 35th IEEE/ACM international conference on automated … , 2020
    2020
    Citations: 280
  • Framer: Planning models from natural language action descriptions
    A Lindsay, J Read, J Ferreira, T Hayton, J Porteous, P Gregory
    Proceedings of the International Conference on Automated Planning and … , 2017
    2017
    Citations: 92
  • Smartbugs 2.0: An execution framework for weakness detection in ethereum smart contracts
    M Di Angelo, T Durieux, JF Ferreira, G Salzer
    2023 38th IEEE/ACM International Conference on Automated Software … , 2023
    2023
    Citations: 52
  • Glitch: Automated polyglot security smell detection in infrastructure as code
    N Saavedra, JF Ferreira
    Proceedings of the 37th IEEE/ACM international conference on automated … , 2022
    2022
    Citations: 51
  • Ecoandroid: An android studio plugin for developing energy-efficient java mobile applications
    A Ribeiro, JF Ferreira, A Mendes
    2021 IEEE 21st international conference on software quality, reliability and … , 2021
    2021
    Citations: 49
  • JaSkel: A Java skeleton-based framework for structured cluster and grid computing
    JF Ferreira, JL Sobral, AJ Proença
    Sixth IEEE International Symposium on Cluster Computing and the Grid (CCGRID … , 2006
    2006
    Citations: 49
  • Visualization of patient behavior from natural language recommendations
    J Siddle, A Lindsay, JF Ferreira, J Porteous, J Read, F Charles, ...
    Proceedings of the 9th Knowledge Capture Conference, 1-4 , 2017
    2017
    Citations: 46
  • Linear logic programming for narrative generation
    C Martens, AG Bosser, JF Ferreira, M Cavazza
    International conference on logic programming and nonmonotonic reasoning … , 2013
    2013
    Citations: 45
  • Automated verification of the FreeRTOS scheduler in Hip/Sleek
    JF Ferreira, C Gherghina, G He, S Qin, WN Chin
    International Journal on Software Tools for Technology Transfer 16 (4), 381-397 , 2014
    2014
    Citations: 42
  • Rango: Adaptive retrieval-augmented proving for automated software verification
    K Thompson, N Saavedra, P Carrott, K Fisher, A Sanchez-Stern, Y Brun, ...
    arXiv preprint arXiv:2412.14063 , 2024
    2024
    Citations: 38
  • Integrating an academic management system with blockchain: A case study
    S Guerreiro, JF Ferreira, T Fonseca, M Correia
    Blockchain: Research and Applications 3 (4), 100099 , 2022
    2022
    Citations: 38
  • Generative story worlds as linear logic programs
    C Martens, JF Ferreira, AG Bosser, M Cavazza
    Seventh Intelligent Narrative Technologies Workshop , 2014
    2014
    Citations: 33
  • Evolution of automated weakness detection in Ethereum bytecode: a comprehensive study
    M Di Angelo, T Durieux, JF Ferreira, G Salzer
    Empirical Software Engineering 29 (2), 41 , 2024
    2024
    Citations: 32
  • On Euclid’s algorithm and elementary number theory
    R Backhouse, JF Ferreira
    Science of Computer Programming 76 (3), 160-180 , 2011
    2011
    Citations: 27
  • Leveraging large language models to boost Dafny’s developers productivity
    ÁF Silva, A Mendes, JF Ferreira
    Proceedings of the 2024 IEEE/ACM 12th International Conference on Formal … , 2024
    2024
    Citations: 24
  • Recounting the rationals: twice!
    R Backhouse, JF Ferreira
    International Conference on Mathematics of Program Construction, 79-91 , 2008
    2008
    Citations: 21
  • Automated narrative planning model extension
    J Porteous, JF Ferreira, A Lindsay, M Cavazza
    Autonomous Agents and Multi-Agent Systems 35 (2), 19 , 2021
    2021
    Citations: 20
  • Narrative planning model acquisition from text summaries and descriptions
    T Hayton, J Porteous, J Ferreira, A Lindsay
    Proceedings of the AAAI Conference on Artificial Intelligence 34 (02), 1709-1716 , 2020
    2020
    Citations: 20
  • Certified password quality: a case study using Coq and Linux pluggable authentication modules
    JF Ferreira, SA Johnson, A Mendes, PJ Brooke
    International Conference on Integrated Formal Methods, 407-421 , 2017
    2017
    Citations: 20