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.
Modern software systems are increasingly analyzed, verified, and repaired using automated reasoning techniques. Most of these techniques, however, rely on simplifying assumptions about program behavior, fault independence, or algorithmic decidability that often fail in realistic software. My research develops the formal and algorithmic foundations needed to reason about these limitations, combining software engineering, formal methods, and program analysis to build techniques that are both theoretically sound and practically applicable.
Software faults rarely occur in isolation. Their interactions, including masking, cascading, and synergistic effects, can fundamentally alter program behavior and undermine conventional approaches to testing, debugging, verification, automated repair, and fault localization. My research develops the formal foundations of fault interaction and translates them into interaction-aware techniques for symbolic execution, program analysis, verification, fuzzing, and automated program repair. The long-term objective is to establish a unified theory of multi-fault software engineering in which analysis and repair reason about interacting faults explicitly rather than assuming their independence.
My second research direction investigates the theoretical limits of automated software reasoning. I study how computability, formal verification, symbolic reasoning, termination analysis, and program semantics shape what automated techniques can guarantee. This includes establishing formal limits such as the undecidability of repair overfitting, developing verification-aware reasoning frameworks, and integrating semantic properties—including correctness, termination, and performance—into automated analysis and synthesis. The broader goal is to design software engineering methods whose guarantees are explicitly aligned with the underlying theory of computation.
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