José João Ferreira
I'm an engineer and researcher focused on formal methods and software verification. My work bridges the gap between theoretical logic and practical system reliability, ranging from developing first-order temporal logic fragments to optimizing MaxSAT solvers. During my Master's, I designed a custom formalism and a high-efficiency tool for validating data-intensive properties in complex systems. I later applied this to validate implementations of public administration protocols in Portugal. Whether I'm benchmarking unsatisfiable core extraction or teaching a Databases course, I enjoy breaking down rigorous scientific concepts into high-impact engineering solutions.
Skills
Fields
Programming
Projects
meta-circular-evaluator-jl
A meta-circular evaluator for a subset of the Julia programming language named MetaJulia with Reflection and Metaprogramming properties as a project for the Advanced Programming course
robotruck-ufo-js
A scene with a robot/truck and a trailer and a scene with a UFO in the countryside in Three.js as a project for the Computer Graphics course
distributed-ledger
A distributed ledger for transactions using gRPC and Maven as a project for the Distributed Systems course
ivm-manager-pgsql
A server-side Intelligent Vending Machine manager in PL/pgSQL accessible by a web application as a project for the Databases course
probability-statistics-r
A set of probabilistic and plotting problems and resolutions using statistical computing and graphics as a computational project for the Probability and Statistics course
takuzu-py
A program that solves the Takuzu problem using A.I. search techniques as a project for the Artificial Intelligence course
Experience
Nov 2025 - Dec 2025 · 2 mos
Pittsburgh, Pennsylvania, United States · On-site
Computer Science Department · Hosted by professor Ruben Martins
Benchmarking two unsatisfiable core extraction methodologies for unweighted MaxSAT. Using the MSU3 algorithm and the Glucose 3 solver via PySAT, we compare the lower bound precision and core minimality of internal solver assumptions against external resolution proof processing with DRAT-trim.
Apr 2025 · Oct 2025 · 7 mos
Lisbon, Portugal · Hybrid
OptiGov Project · Supervised by professor Alessandro Gianola
Applying ACTLChecker to validate a rigorous implementation of the BPMN of the ICT Approval Protocol at IGFEJ, a public body under the Portuguese Ministry of Justice, by checking concurrent logs against property specifications in Action Temporal Logic, a formalism created in my master's thesis.
Apr 2025 Jul 2025 · 4 mos
Lisbon, Portugal · On-site
Databases Course · Undergraduate, Computer Science and Engineering
Instructing lab sessions and coordinating student groups in the design of relational databases, guiding entity-relationship modeling, schema normalization, transaction processing, and concurrency control while providing technical support for SQL implementation, project evaluation, and exam proctoring.
Education
Sep 2023 - Nov 2025
Alameda · Lisbon, Portugal
Grade: 17.35
Oct 2020 - Jul 2023
Alameda · Lisbon, Portugal
Grade: 16.12
