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
Latest
- 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
- Leveraging Large Language Models to Boost Dafny's Developers Productivity
- DifFuzzAR: automatic repair of timing side-channel vulnerabilities via refactoring
- 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
- 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
- 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
- Towards Improving the Usability of Password Managers
- Automated narrative planning model extension
- SmartBugs: A Framework to Analyze Solidity Smart Contracts
- 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
- SmartBugs: An Execution Framework for Automated Analysis of Smart Contracts
- Skeptic: Automatic, Justified and Privacy-Preserving Password Composition Policy Selection
- Extending Narrative Planning Domains with Linguistic Resources
- Narrative Planning Model Acquisition from Text Summaries and Descriptions
- Logic, Algebra, and Geometry at the Foundation of Computer Science
- Lost in Disclosure: On The Inference of Password Composition Policies
- Open and Interactive Learning Resources for Algorithmic Problem Solving
- GPS+: Reasoning About Fences and Relaxed Atomics
- Towards a Program Logic for C11 Release-Sequences
- Towards Verified Handwritten Calculational Proofs
- Certified Password Quality: A Case Study Using Coq and Linux Pluggable Authentication Modules
- Framer: Planning Models from Natural Language Action Descriptions
- ReqCap: Hierarchical Requirements Modeling and Test Generation for Industrial Control Systems
- StoryFramer: From Input Stories to Output Planning Models
- Towards a Constraints Approach to Generating Personalised Horror Film Variants
- Visualization of Patient Behavior from Natural Language Recommendations
- A calculational approach to path-based properties of the Eisenstein-Stern and Stern-Brocot trees via matrix algebra
- Reasoning about Fences and Relaxed Atomics
- Supporting Social Skills Rehabilitation with Virtual Storytelling
- Automated Verification of the FreeRTOS Scheduler in HIP/SLEEK
- Structure Editing of Handwritten Mathematics: Improving the Computer Support for the Calculational Method
- The Magic of Algorithm Design and Analysis: Teaching Algorithmic Skills using Magic Card Tricks
- Generative Story Worlds as Linear Logic Programs
- The Algorithmics of Solitaire-Like Games (Extended Version)
- Linear logic programming for narrative generation
- Deadline analysis of AUTOSAR OS periodic tasks in the presence of interrupts
- Automated Verification of the FreeRTOS Scheduler in HIP/SLEEK
- An Improved Proof of the Handshaking Lemma
- Principles and Applications of APS
- On Euclid's Algorithm and Elementary Number Theory
- Logic Training through Algorithmic Problem Solving
- Principles and Applications of Algorithmic Problem Solving
- Designing an Algorithmic Proof of the Two-Squares Theorem
- The Algorithmics of Solitaire-Like Games
- Probabilities in Proofreading
- Students' Feedback on Teaching Mathematics Through The Calculational Method
- Which Mathematics for the Information Society?
- Multiples in the Fibonacci Series
- JFF7: An exercise from "The Art of Computer Programming"
- A Reward Check From Donald Knuth
- A Square Grid Path Problem
- Recounting the Rationals: Twice!
- JFF6: Resolução eficaz de problemas, quatro exemplos
- JFF1: Exchanging the values of two variables
- JFF0: Distributivity and the greatest common divisor
- JaSkel: A Java Skeleton-Based Framework for Structured Cluster and Grid Computing
- A contribution towards a Distributed Java Virtual Machine
- ParC#: Parallel Computing with C# in .NET
- Camila Revival: VDM meets Haskell