Here you can find information about some of my current projects and members of my research group.

Research Projects

Learning and Adapting Formal Specifications

Formal specifications underpin the synthesis and verification of software systems, yet correct specifications are hard to write and rarely stay correct as systems and their environments evolve. We study how formal specifications can be learned, repaired and adapted, combining automated reasoning with learning-based techniques. Our work ranges from understanding what learners can capture and generalise over formal languages, to verification-guided methods that diagnose and resolve flaws in specifications and keep them fit for purpose as the conditions they rely on change.

Collaborators

Relevant papers

  • Charles Pert, Dalal Alrajeh, Alessandra Russo. Transition-Based Acceptance for ω-Regular Expression Synthesis. Formal Aspects of Computing 38(3), 2026.
  • Tiberiu Georgescu, Alexander W. Goodall, Dalal Alrajeh, Francesco Belardinelli, Sebastián Uchitel. Adaptive GR(1) Specification Repair for Liveness-Preserving Shielding in Reinforcement Learning. NeSy 2026.
  • Francisco Cirelli, Dalal Alrajeh, Sebastián Uchitel. Unavoidable Boundary Conditions: A Control Perspective on Goal Conflicts. ICSE 2025.
  • Titus Buckworth, Dalal Alrajeh, Jeff Kramer, Sebastián Uchitel. Adapting Specifications for Reactive Controllers. SEAMS 2023.
  • Davide G. Cavezza, Dalal Alrajeh, András György. A Weakness Measure for GR(1) Formulae. Formal Aspects of Computing 33(1), 2021.
  • Dalal Alrajeh, Antoine Cailliau, Axel van Lamsweerde. Adapting Requirements Models to Varying Environments. ICSE 2020.

Requirements Engineering for AI-enabled Systems

While significant effort has gone into testing and verifying machine learning systems, far less has focused on modelling and verifying their requirements, especially when these systems depend on evolving data and work alongside people whose expertise, judgement and intent shape how they behave. Our interdisciplinary research develops methods for the (semi-)formal elicitation, traceability, verification and repair of requirements for AI-enabled systems, from decision-support tools developed with law enforcement practitioners to autonomous drones that must translate human instructions into safe manoeuvres.

Collaborators

Relevant papers

  • Jessica Woodhams, Amy Burrell, Wanyin Li, Fahim Ahmed, Matthew Tonkin et al., Dalal Alrajeh. How Analysts Use AI in High-Stakes Crime Linkage: An Industrial Study. FSE 2026 (Industry track).
  • Dalal Alrajeh, Vesna Nowack, Patrick Benjamin et al. Data-Dependent Goal Modeling for ML-Enabled Law Enforcement Systems. ICSE SEIS 2026.
  • Yicheng Zhan, Fahim Ahmed, Amy Burrell, Matthew Tonkin, Sarah Galambos, Jessica Woodhams, Dalal Alrajeh. Enhancing Binary Encoded Crime Linkage Analysis Using Siamese Network. AAAI 2026.
  • Vesna Nowack, Dalal Alrajeh et al. Towards User-Centred Design of AI-Assisted Decision-Making in Law Enforcement. EASE 2025.
  • Sofia Nelson, Dalal Alrajeh, Pedro Alarcon Granadeno, Jane Cleland-Huang. A Model for Mediating Multi-Modal Human Intent into Safe Maneuvers for UAVs. RE Workshops 2026.

Normative Requirements for Autonomous Systems

Autonomous systems increasingly need to follow social, legal, ethical, empathetic and cultural (SLEEC) rules. We develop formal techniques to check that such rules are consistent and realizable, and to diagnose and resolve conflicts between them.

Collaborators

  • Marsha Chechik, University of Toronto, Canada
  • Lina Marsso, Polytechnique Montréal, Canada
  • Nick Feng, Amazon Web Services

Relevant papers

  • Junwei Quan, Lina Marsso, Dalal Alrajeh, Marsha Chechik. Untangling Shared Phenomena for Improving Analysis of Normative Requirements. MO2RE 2025.

Causal Explanation of System Behaviour

When a software or AI-enabled system violates its specification, engineers need to know why, and what to change. We develop formal accounts of actual causality that explain system failures and the counterexamples produced by verification tools, combine the causal judgements of different experts about how a system behaves, and reason about interventions, the changes to a system or its environment that would prevent a violation, to guide diagnosis and repair.

Collaborators

  • Robert Craven, Imperial College London, UK

Relevant papers

  • Daniel Özcan, Dalal Alrajeh, Robert Craven. Reasoning about Actual Causality in Answer Set Programming. KR 2025.
  • Herong Meng, Dalal Alrajeh. Causal Detection in Linear Temporal Counterexamples. FSE 2025 Companion.
  • Dalal Alrajeh, Hana Chockler, Joe Halpern. Combining Experts' Causal Judgments. Artificial Intelligence, 2020.

Group members

Current members

  • Dr Vesna Nowack, Research Associate
  • Charles Pert, PhD Candidate, Teaching Scholar
  • Tiberiu Georgescu, PhD Candidate, STAI CDT Scholar

Past members

  • Dr Rakhilya Mekhtieva, PhD Student, AI4Health CDT Scholar
  • Fahim Ahmed, Research Assistant
  • Daniel Özcan, Research Assistant
  • Yicheng Zhan, Research Assistant
  • Dr Zhi Zhang, Research Associate
  • Nicolas Gray, Research Assistant
  • Ares Agourides, Research Software Engineer
  • Théophile Sautory, Research Assistant
  • Ludovico Mitchener, Research Assistant
  • Patrick Benjamin, Research Assistant
  • Dr Pawel Gomoluch, PhD Student
  • Dr Davide Cavezza, PhD Student, HiPEDS CDT Scholar
  • Kari Davies, Research Assistant