João F. Ferreira
João F. Ferreira
Latest posts
ProfOlaf: Semi-Automated Tool for Systematic Literature Reviews
The Ultimate Configuration Management Tool? Lessons from a Mixed Methods Study of Ansible's Challenges
Vibenix: An AI Assistant for Software Packaging with Nix
ICSE 2020 paper is the most cited according to 2025 Scholar Metrics
I’m happy to share that, according to the 2025 Scholar Metrics : Our paper “ Empirical Review of Automated Analysis Tools on 47,587 Ethereum Smart Contracts ” (T. Durieux, J.F. Ferreira, R. Abreu, P. Cruz – ICSE 2020) is the most cited paper from ICSE! And our paper “ SmartBugs: A Framework to Analyze Solidity Smart Contracts ” (J.F. Ferreira, P. Cruz, T. Durieux, R.…
Awarded an Amazon Research Award on Automated Reasoning!
I’m excited to share that I’ve received an Amazon Research Award on Automated Reasoning! The award will support my research on automated program repair for Infrastructure as Code. The first steps of this research have already been completed, and we will be presenting our early results and our tool, InfraFix , at ISSTA later this month. InfraFix is a collaboration with Nuno Saavedra and Alexandra…
Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification
InfraFix: Technology-Agnostic Repair of Infrastructure as Code
ACM SIGSOFT Distinguished Paper Award at ICSE 2025
Our paper “ Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification ” has received an ACM SIGSOFT Distinguished Paper Award at ICSE 2025. The paper introduces an innovative automated proof synthesis tool that uses machine learning and large language models with retrieval augmentation techniques. Rango dynamically identifies and incorporates relevant proofs and…
Do Experts Agree About Smelly Infrastructure?
InfraGov: New Funded Project on Reliable and Secure IT Infrastructure
I am very pleased to announce that we secured funding for the InfraGov project , a new research project funded to address critical challenges in the reliability and security of Infrastructure as Code (IaC) used in Public Administration. As more public services move to cloud-based and digital platforms, the integrity of configuration and infrastructure code becomes essential to safeguard sensitive…
Contract Usage and Evolution in Android Mobile Applications
CoqPyt: Proof Navigation in Python in the Era of LLMs
How are Contracts Used in Android Mobile Applications?
Evolution of automated weakness detection in Ethereum bytecode: a comprehensive study
AI for Formal Verification
We build AI-assisted tools for proof engineering and verification-aware programming languages. This work explores how large language models, retrieval, programmatic proof interaction, and verification feedback can reduce the effort required to develop and maintain formally verified software. See the posts and publications below for more details.
Leveraging Large Language Models to Boost Dafny's Developers Productivity
DifFuzzAR: automatic repair of timing side-channel vulnerabilities via refactoring
Related Automatic Repair of Java Code with Timing Side-Channel Vulnerabilities (2021)
Polyglot Code Smell Detection for Infrastructure as Code with GLITCH
SmartBugs 2.0: An Execution Framework for Weakness Detection in Ethereum Smart Contracts
Hoogle⋆: Constants and λ-abstractions in Petri-net-based Synthesis using Symbolic Execution
MUFIN: Improving Neural Repair Models with Back-Translation
bGSL: An Imperative Language for Specification and Refinement of Backtracking Programs
Related A wp Calculus for a Preferential Computations: Mechanisation in Isabelle/HOL (Technical report)
GLITCH: Automated Polyglot Security Smell Detection in Infrastructure as Code
Extending EcoAndroid with Automated Detection of Resource Leaks
Verified password generation from password composition policies
A Preliminary Study on Generating Well-Formed Q# Quantum Programs for Fuzz Testing
Reliable DevOps
We work on methods and tools to increase the reliability of Infrastructure as Code artifacts. See the posts and publications below for more details.
EcoAndroid: An Android Studio Plugin for Developing Energy-efficient Java Mobile Applications
Exploring Usable Security to Improve the Impact of Formal Verification: A Research Agenda
Formal Methods Teaching: 4th International Workshop and Tutorial (FMTea 2021)
Automatic Repair of Java Code with Timing Side-Channel Vulnerabilities
Related DifFuzzAR: automatic repair of timing side-channel vulnerabilities via refactoring (2024)
Towards Improving the Usability of Password Managers
Automated narrative planning model extension
SmartBugs: A Framework to Analyze Solidity Smart Contracts
Related Empirical Review of Automated Analysis Tools on 47,587 Ethereum Smart Contracts Summary of contributions and findings
Evaluating the Accuracy of Password Strength Meters using Off-The-Shelf Guessing Attacks
Empirical Review of Automated Analysis Tools on 47,587 Ethereum Smart Contracts
Related Summary of contributions and findings
Teaching
I am an Associate Professor at the Faculty of Engineering , University of Porto . Previously, I was an Associate Professor at Instituto Superior Técnico , University of Lisbon . Before that, I worked in the UK Higher Education (HE) environment for 12 years, since my first teaching experiences at the University of Nottingham. After obtaining my Postgraduate Certificate in Learning and Teaching in…
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…
Skeptic: Automatic, Justified and Privacy-Preserving Password Composition Policy Selection
Errata Correction concerning the source of the datasets used (it does not affect the conclusions of the work)
Smartbugs
SmartBugs is an execution framework that simplifies the execution of automated analysis tools on datasets of Solidity smart contracts. For more details, see list of publications below or visit SmartBugs’s webpage .
Extending Narrative Planning Domains with Linguistic Resources
Related Automated narrative planning model extension. In Autonomous Agents (2021)
Narrative Planning Model Acquisition from Text Summaries and Descriptions
Research Opportunities
I am always looking for new talented research students and post-doc researchers. See below for more details on current opportunities, examples of previous work, and information on working at INESC-ID and living in Lisbon. If you are interested in working with me, get in touch ! See also the page of my group, the Software Reliability Lab , for more information on our research and projects. Current…
Logic, Algebra, and Geometry at the Foundation of Computer Science
Lost in Disclosure: On The Inference of Password Composition Policies
Errata Correction concerning the source of the datasets used (it does not affect the conclusions of the work)