Omar I. Al-Bataineh — Gran Sasso Science Institute, Italy
Vision
Automated software engineering techniques — repair, testing, symbolic
execution, and verification — are increasingly relied upon to reason
about real software, yet most of them rest on simplifying assumptions:
that faults are independent, that local correctness composes, or that
the underlying decision problems are tractable. These assumptions
break down in realistic, multi-fault, and formally rich settings. The
problems below outline what I see as the fundamental open questions
standing between today's automated techniques and the guarantees
practitioners actually need. They define the long-term research
program I am building, organized around the two themes introduced on
my homepage.
This page summarizes research problems that I believe represent
promising long-term directions for the software engineering and
formal methods communities. Some are active topics in my current
research, while others are intended to stimulate broader discussion
and collaboration.
Figure 1. The research agenda organized around two themes and their constituent open problems.
Suitable for MSc Suitable for PhD Collaboration welcome Representative papers
Theme I: Foundations of Interaction-Aware Software Engineering
Faults rarely occur in isolation, and their interactions — masking,
cascading, and synergistic effects — can fundamentally alter program
behavior. Yet most analysis, testing, and repair techniques are
designed and evaluated under an implicit single-fault assumption,
treating co-occurring faults in multi-fault programs as if they act
independently. The challenges below ask what changes — technically
and formally — once fault interaction, rather than mere co-occurrence,
is taken seriously.
Challenge 1 — Repair Compatibility Status: Open (Foundational)
Research Question
When do independently correct repairs remain correct once composed into the same system?
Why It Is Difficult
Compatibility is a relational property of the composed program, not of either repair alone — two repairs can each satisfy their own specification while still violating a global property that neither one was designed to preserve.
Why Existing Techniques Fall Short
Standard repair pipelines generate and validate patches independently against local test suites, with no mechanism for reasoning about cross-repair interaction after deployment.
Possible Research Directions
Identifying decidable compatibility fragments (e.g., repairs with disjoint semantic footprints), sound approximations for the general case, and compatibility-aware repair generation that treats composition as a first-class constraint.
Long-Term Vision
A principled foundation for multi-fault repair pipelines, replacing an implicit and often-violated assumption with explicit, checkable guarantees.
Suitable for PhD · Collaboration welcome
Challenge 2 — Interaction-Aware Symbolic Execution Status: Open (Foundational)
Research Question
How should symbolic execution explore and represent program behavior when multiple faults interact along the same execution paths?
Why It Is Difficult
Classical symbolic execution treats each path condition independently; when faults mask, cascade, or combine, the resulting symbolic state no longer decomposes cleanly per fault, and path explosion is compounded by fault interaction.
Why Existing Techniques Fall Short
Existing symbolic execution engines are built around single-fault triage and localization, offering no explicit model of how multiple faulty regions jointly constrain program behavior.
Possible Research Directions
Interaction-aware path prioritization, compositional symbolic summaries for interacting fault regions, and formal characterizations of when fault interactions can be decomposed safely.
Long-Term Vision
More accurate fault localization and patch validation for realistic, multi-fault programs, where current symbolic techniques are known to underperform.
Suitable for PhD · Collaboration welcome
Challenge 3 — Formal Models of Fault Interaction Status: Open (Exploratory)
Research Question
Can fault interaction — masking, cascading, and synergistic effects between faults — be given a general formal semantics, rather than being studied case by case?
Why It Is Difficult
Interaction effects are highly context-dependent: the same pair of faults may mask each other under one input distribution and compound under another, resisting a single static characterization.
Why Existing Techniques Fall Short
Empirical studies document interaction effects convincingly but largely stop short of a semantic model that predicts when and why they arise, limiting generalization beyond the studied programs.
Possible Research Directions
A semantic taxonomy of interaction types grounded in program state and execution traces, and formal conditions under which two faults are guaranteed to be non-interacting.
Long-Term Vision
A unifying theory that testing, debugging, fault localization, and repair techniques could all build on, rather than each rediscovering interaction effects independently.
Suitable for MSc · Suitable for PhD · Collaboration welcome · Related work below
Theme II: Foundations of Automated Reasoning and Decidability
Automated repair, testing, and verification techniques implicitly
promise guarantees they cannot always deliver. The challenges below
ask where the boundary between tractable and fundamentally impossible
actually lies, and how to design techniques that respect it.
Challenge 4 — Decidable Repair Fragments Status: Open (Active)
Research Question
Beyond knowing that general repair-correctness and repair-compatibility problems are undecidable, which restricted classes of repairs admit decidable, checkable guarantees?
Why It Is Difficult
Undecidability results (including the undecidability of overfitting and of repair compatibility) hold for unrestricted repairs; identifying useful decidable fragments requires restrictions that are both formally tractable and representative of how repairs are generated in practice.
Why Existing Techniques Fall Short
Practical repair tools sidestep decidability entirely, relying on heuristics and test-suite validation with no explicit account of what can or cannot be guaranteed for the class of repairs they generate.
Possible Research Directions
A taxonomy of repair classes (bounded edit locations, template-based repairs, disjoint-footprint repairs) paired with the strongest guarantee decidable for each, rather than a search for a universal checker.
Long-Term Vision
Repair systems that can honestly state what they guarantee for a given class of repairs, instead of implying guarantees that undecidability rules out in general.
Suitable for PhD · Collaboration welcome · Representative paper below
Challenge 5 — Compositional Patch Correctness Status: Open (Exploratory)
Research Question
Can patch correctness be verified compositionally — establishing global correctness from local, per-patch proof obligations — for realistic multi-patch systems?
Why It Is Difficult
Compositional verification frameworks (assume-guarantee reasoning, interface automata) were developed for hand-written component contracts; automatically generated patches rarely come with contracts strong enough to support this style of reasoning.
Why Existing Techniques Fall Short
Program repair and compositional verification have developed largely as separate communities, and existing repair validation does not produce artifacts — contracts, interfaces, or invariants — that a compositional verifier could consume.
Possible Research Directions
Repair techniques that synthesize lightweight local contracts alongside patches, and verification procedures adapted to reason over such contracts under composition.
Long-Term Vision
A bridge between automated repair and formal verification, moving patch validation from empirical testing toward auditable correctness arguments.
Suitable for PhD · Collaboration welcome
Challenge 6 — Verification-Aware Program Repair Status: Open (Exploratory)
Research Question
How should model checking and specification languages be extended to reason natively about interacting faults and the repairs applied to them, rather than treating each fix as an isolated model update?
Why It Is Difficult
Model checking scales by exploiting structure in the model; treating every repair as an arbitrary perturbation to be re-verified from scratch forfeits that structure and reintroduces state-space explosion at every repair step.
Why Existing Techniques Fall Short
Verification tools are largely repair-agnostic, and repair tools are largely verification-agnostic; neither side offers incremental or interaction-aware guarantees when multiple fixes are applied over time.
Possible Research Directions
Fault-aware specification languages that make interaction assumptions explicit, and incremental verification procedures that reuse prior verification effort across sequential or composed repairs.
Long-Term Vision
Verified multi-fault repair as a practical possibility rather than a purely theoretical goal, with verification cost that scales with the size of a repair rather than the size of the system.
Suitable for PhD · Collaboration welcome
Opportunities for Collaboration
These challenges span software engineering, formal methods, program
analysis, and the theory of computation, and I expect progress on
most of them to require genuinely cross-disciplinary collaboration.
I am glad to discuss any of the challenges above in more depth,
whether the interest is theoretical (formal models, decidability,
compositional verification) or systems-oriented (building
interaction-aware tools for repair, testing, or symbolic execution).
Interested Students
Several of these challenges are well suited to PhD or MSc research,
ranging from focused technical questions (e.g., decidable fragments
of a specific challenge) to more open-ended exploratory work. If you
are a student interested in formal methods, program analysis, or
automated program repair and would like to discuss a potential
project connected to any of the challenges above, please get in
touch.
Research Philosophy
My research keeps returning to one question: what are the fundamental
limits of automated software engineering, and how can techniques be
designed so that their guarantees are explicit rather than assumed?
This question runs through my work on repair compatibility, the
undecidability of patch overfitting, decidable repair fragments, fault
interaction, and verification-aware repair — each asks not only
whether a technique works in practice, but what it can and cannot
guarantee in principle.
I believe this distinction matters because automated techniques are
increasingly trusted with decisions that once required human judgment.
Software engineering should meet that responsibility with rigor:
characterizing precisely where guarantees hold, where they break down,
and what it would take to restore them — rather than treating
correctness as an empirical accident of testing.