Set of Support for Higher-Order Reasoning. - Ahmed Bhayat; Giles Reger (PAAR@FLoC, 2018)

Restricted Combinatory Unification. - Ahmed Bhayat; Giles Reger (CADE, 2019)

A Knuth-Bendix-Like Ordering for Orienting Combinator Equations. - Ahmed Bhayat; Giles Reger (IJCAR (1), 2020)

A Combinator-Based Superposition Calculus for Higher-Order Logic. - Ahmed Bhayat; Giles Reger (IJCAR (1), 2020)

A Polymorphic Vampire - (Short Paper). - Ahmed Bhayat; Giles Reger (IJCAR (2), 2020)

FuSeBMC: An Energy-Efficient Test Generator for Finding Security Vulnerabilities in C Programs. - Kaled M. Alshmrany; Mohannad Aldughaim; Ahmed Bhayat; Lucas C. Cordeiro (TAP@STAF, 2021)

FuSeBMC v.4: Smart Seed Generation for Hybrid Fuzzing. - Kaled M. Alshmrany; Mohannad Aldughaim; Ahmed Bhayat; Lucas C. Cordeiro (CoRR, 2021)

Automated theorem proving in higher-order logic - Ahmed Bhayat (2021)

FuSeBMC v4: Smart Seed Generation for Hybrid Fuzzing - (Competition Contribution). - Kaled M. Alshmrany; Mohannad Aldughaim; Ahmed Bhayat; Lucas C. Cordeiro (FASE, 2022)

The Rapid Software Verification Framework. - Pamina Georgiou; Bernhard Gleiss; Ahmed Bhayat; Michael Rawson 001; Laura Kovács; Giles Reger (FMCAD, 2022)

Lemmaless Induction in Trace Logic. - Ahmed Bhayat; Pamina Georgiou; Clemens Eisenhofer; Laura Kovács; Giles Reger (CICM, 2022)

Position Paper: Towards a Hybrid Approach to Protect Against Memory Safety Vulnerabilities. - Kaled M. Alshmrany; Ahmed Bhayat; Franz Brauße; Lucas C. Cordeiro; Konstantin Korovin; Tom Melham; Mustafa A. Mustafa; Pierre Olivier; Giles Reger; Fedor Shmarov (SecDev, 2022)

FuSeBMC v4: Improving code coverage with smart seeds via fuzzing and static analysis. - Kaled M. Alshmrany; Mohannad Aldughaim; Ahmed Bhayat; Fedor Shmarov; Fatimah Aljaafari; Lucas C. Cordeiro (CoRR, 2022)

Superposition with Delayed Unification. - Ahmed Bhayat; Johannes Schoisswohl; Michael Rawson 001 (CADE, 2023)

Refining Unification with Abstraction. - Ahmed Bhayat; Konstantin Korovin; Laura Kovács; Johannes Schoisswohl (LPAR, 2023)

A Higher-Order Vampire (Short Paper). - Ahmed Bhayat; Martin Suda 001 (IJCAR (1), 2024)

LLM-Generated Invariants for Bounded Model Checking Without Loop Unrolling. - Muhammad A. A. Pirzada; Giles Reger; Ahmed Bhayat; Lucas C. Cordeiro (ASE, 2024)

FuSeBMC v4: Improving Code Coverage with Smart Seeds via BMC, Fuzzing and Static Analysis. - Kaled M. Alshmrany; Mohannad Aldughaim; Ahmed Bhayat; Lucas C. Cordeiro (Formal Aspects Comput., 2024)

The Vampire Diary. - Filip Bártek; Ahmed Bhayat; Robin Coutelier; Márton Hajdú; Matthias Hetzenberger; Petra Hozzová; Laura Kovács; Jakob Rath; Michael Rawson 001; Giles Reger; Martin Suda 001; Johannes Schoisswohl; et al. (CAV (3), 2025)