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 in leading software engineering venues including ICSE, ASE, TOSEM, SANER, ICSME, FASE, JSS, and ACM TECS.
I earned my Ph.D. in Computer Science from the University of Western Australia, an M.Sc. from the University of New South Wales, and a B.Sc. in Computer Engineering from Jordan University of Science and Technology. 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 challenge conventional approaches to testing, debugging, verification, automated repair, and fault localization. My research develops formal foundations for 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 foundation for software engineering in which analysis and repair explicitly account for interacting faults 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.
These two threads feed into a broader, long-term research agenda — a living collection of open problems spanning multi-fault software engineering, automated program repair, symbolic execution, software verification, fuzzing, and the theoretical foundations of automated software reasoning, motivating future work and potential collaborations.
We establish that determining whether an automated program repair system will overfit is undecidable in general, characterizing fundamental limits on fully automated patch validation.
We develop a formal model of interacting faults and show how masking, synergy, and cascading effects undermine conventional debugging and automated repair approaches for multi-fault programs.
We investigate how interactions among multiple faults affect patch assessment and motivate validation techniques that account for fault interactions rather than treating faults independently.
We formulate interaction-aware validation oracles for multi-fault program repair, accounting for masking, synergy, cascading, and independence among faults.
We investigate the relationship between automated program repair and program termination, and extend test-based patch validation with oracles for the absence of erroneous behavior and successful termination of the patched program.
We describe a repair framework that uses program slicing to eliminate code irrelevant to the target bug, reducing the repair problem while preserving the ability to generate correct patches.
We provide a formal characterization of performance bugs and their behavioral consequences, establishing a foundation for reasoning about performance-related defects.
We investigate invariant-based reasoning as a foundation for automated program repair, using behavioral invariants to guide and constrain the repair process.
We devise a bug classification system for bugs that lack observable erroneous behavior (e.g. termination and non-functional bugs) and show that integrating dynamic APR with formal analysis techniques such as termination provers and model checkers extends the range of bugs APR can handle.
We explore how automated program repair can be extended to address bug classes beyond those traditionally handled by existing repair approaches.
We present the first general-purpose, gas-aware automated smart contract repair approach, using a search-based method guided by a novel gas dominance relationship among candidate patches.
My research spans the software engineering and formal methods communities, with active collaborations across both.
I welcome opportunities to collaborate with researchers and highly motivated students on challenging problems in software engineering, formal methods, program analysis, software verification, automated program repair, symbolic execution, software testing, and related areas.
Email: omar.albataineh@gssi.it