Omar I. Al-Bataineh
Research Scientist at the Gran Sasso Science Institute, Italy
Research Scientist at the Gran Sasso Science Institute, Italy
I am a Research Scientist at the Gran Sasso Science Institute (GSSI), Italy, working on the foundations of automated program analysis. My research develops formal and algorithmic frameworks for automated program repair, fault interaction, and software verification — with a particular focus on settings where classical single-fault assumptions break down and standard correctness guarantees no longer hold. My work has appeared at ICSE, ASE, TOSEM, SANER, and ICSME.
I earned my Ph.D. in Computer Science from the University of Western Australia. Prior to GSSI, I held research positions at Simula Research Laboratory (Norway), the National University of Singapore, and Nanyang Technological University — collaborating across the software engineering and formal verification communities.
Most automated program analysis techniques are built on a silent assumption: faults are independent, and fixing one does not affect the others. In practice, this assumption routinely fails. Faults mask each other, cascade across components, and interact in ways that invalidate isolated diagnoses and render standard correctness guarantees unsound. My research develops the formal and algorithmic foundations needed to reason about programs in the presence of fault interaction — reconsidering the theoretical basis of automated repair, verification, and analysis from the ground up.
When multiple faults co-exist in a program, their interactions produce emergent behaviours — masking, cascading, and synergistic effects — that defeat standard fault localisation and repair pipelines. A patch that corrects one fault in isolation may be invalidated, obscured, or rendered semantically unsound by the presence of others. This line of work builds a formal theory of fault interaction and translates it into interaction-aware repair methods: diagnostics that explicitly model fault dependencies, lightweight oracles that track interaction structure across the patch search space, and patch assessment criteria that verify correctness under composition rather than in isolation. The goal is a repair framework that is robust by construction in multi-fault settings, not merely effective on single-fault benchmarks.
The dominant empirical paradigm in automated repair — generate a patch, validate it against a test suite, ship it — rests on an assumption that test-suite adequacy is a proxy for semantic correctness. It is not, and the reason is fundamental: general patch correctness is undecidable. Plausible patches that overfit to available tests are not an engineering shortcoming to be fixed with better test suites; they are a structural consequence of the underlying computability landscape. This work makes that boundary explicit. It develops undecidability-aware repair frameworks that confine synthesis to decidable program fragments, introduces ROF as a formally grounded measure of overfitting risk, and establishes conditions under which stronger patch correctness guarantees are achievable in principle. The practical target is repair tooling that is honest about what it can and cannot guarantee — a prerequisite for deployment in safety-critical systems.
Correctness is necessary but not sufficient. A patch that restores functional behaviour while introducing non-termination, performance regression, or unsafe resource consumption is not a repair — it is a trade. Classical repair frameworks treat termination and performance as orthogonal concerns, addressed separately or not at all. This work integrates termination analysis and formal performance reasoning directly into the repair loop, ensuring that generated patches satisfy not just the target specification but also liveness and efficiency constraints. The result is a repair model that is simultaneously correct, terminating, and resource-aware — properties that must be jointly verified for deployment in real-world, long-running, or resource-constrained systems.
My research spans the software engineering and formal methods communities, with active collaborations across both.
For a complete list, visit my DBLP profile.
Email: omar.albataineh@gssi.it