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
- 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