Dr Vasileios Klimis
Lecturer in Computer Science
School of Electronic Engineering and Computer Science
Queen Mary University of London
Research
Formal Methods/ Fuzz Testing/ Verification/ Validation/, Programming Languages/ Networking Implementations/ Weak Memory Models/ RDMA (Remote Direct Memory Access)/ Quantum Computing
Interests
I explore novel ways to apply formal methods, logical frameworks, and programming language technology to advance fuzz testing, verification, and validation across a range of systems — including networking stacks, GPU compilers, weak memory models, RDMA configurations, and quantum computing environments.
Publications

Publications of specific relevance to the Centre for Fundamentals of AI and Computational Theory
2025
A Low-Latency Control Fabric for Distributed Quantum Error Correction using RDMA: A Timed Event Structure ModelKlimis V
IEEE International Conference on Pervasive Intelligence and Computing (PICom).
21-10-2025
Shaking Up Quantum Simulators with Fuzzing and Rigour Proceedings of The Conference on Object-Oriented Programming Systems, Languages, and Applications, Oopsla,
Association For Computing Machinery (Acm) vol. 9
09-10-20252024
Semantics of Remote Direct Memory Access: Operational and Declarative Models of RDMA on TSO ArchitecturesKlimis V
The ACM SIGPLAN International Conference on Systems, Programming, Languages and Applications: Software for Humanity (SPLASH) / OOPSLA.
21-10-2024
Lost in Interpretation: Navigating Challenges in Validating Persistency
Models Amid Vague Specs and Stubborn Machines, All with a Sense of HumourKlimis V Donaldson AF Vafeiadis V Wickerson J Raad A
28-05-2024
Challenges in Empirically Testing Memory Persistency ModelsKlimis V Donaldson AF Vafeiadis V Wickerson J Raad A
Proceedings of the 2024 ACM/IEEE 44th International Conference on Software Engineering: New Ideas and Emerging Results., 82-86.
14-04-2024
Chasing Unicorns and Not Losing Hope in Validating Weak Memory Persistency ModelsKlimis V
15-01-20242023
Taking Back Control in an Intermediate Representation for GPU ComputingKlimis V Clark J Baker A Neto D Wickerson J Donaldson AF
Proceedings of The Acm on Programming Languages,
Association For Computing Machinery (Acm) vol. 7 (POPL), 1740-1769.
09-01-20232020
Model Checking Software-Defined Networks with Flow Entries that Time OutKlimis V Parisis G Reus B
Formal Methods in Computer-Aided Design – FMCAD.
05-10-2020
Model Checking Software-Defined Networks with Flow Entries that Time Out
(version with appendix)Klimis V Parisis G Reus B
14-08-2020
Towards Model Checking Real-World Software-Defined Networks (version
with appendix)Klimis V Parisis G Reus B
24-04-2020
A Compositional Approach to Quantitative Verification of Software-defined NetworksKlimis V
13-04-2020
Towards Model Checking Real-World Software-Defined NetworksKlimis V Parisis G Reus B
Lecture Notes in Computer Science. vol. 12225, 126-148.
01-01-2020
Artifact for Taking Back Control in an Intermediate Representation for GPU ComputingKlimis V Donaldson A Clark J Baker A Neto D Wickerson J
Shouting at Memory: Where Did My Write Go? Ecoop
Research Group