Dr Florian Furbach
Pronouns: He/Him
Academic and research departments
Computer Science Research Centre, School of Computer Science and Electronic Engineering.About
Biography
I am a Postdoctoral Research Fellow in Computer Science at the ¿Û¿Û´«Ã½ and a member of the ¿Û¿Û´«Ã½ Centre for Cyber Security. My research focuses on formal verification of concurrent and distributed systems, with particular expertise in weak memory models, program verification, and automated reasoning. I earned my PhD in Computer Science from TU Kaiserslautern. I previously held postdoctoral positions at the Technical University of Denmark and Uppsala University, as well as research positions at TU Kaiserslautern and TU Braunschweig. I develop theory and practical tools for verifying correctness and portability of concurrent software. I co-developed Dartagnan, a tool for verifying concurrent programs.
ResearchResearch interests
Distributed Programming
I design and analyse scalable approaches for distributed systems, with a focus on swarm-based coordination and high-performance communication. My current work concentrates on RDMA-based systems, particularly fault scenarios, interactions with shared memory, and the formal verification of RDMA communication models and libraries.
Program Verification
I study a broad range of verification problems for concurrent programs, combining formal methods with practical tool support. My work spans model checking, systematic testing, control-state reachability, and portability analysis, with an emphasis on efficient encodings and automated reasoning techniques.
Weak Memory Models
I specialise in the verification of concurrent programs under weak memory semantics, particularly x86/TSO and related architectures. I have investigated the computational complexity of key verification tasks—such as testing, reachability, and portability—and developed SMT-based methods and tools that enable scalable automated verification under these models.
Research interests
Distributed Programming
I design and analyse scalable approaches for distributed systems, with a focus on swarm-based coordination and high-performance communication. My current work concentrates on RDMA-based systems, particularly fault scenarios, interactions with shared memory, and the formal verification of RDMA communication models and libraries.
Program Verification
I study a broad range of verification problems for concurrent programs, combining formal methods with practical tool support. My work spans model checking, systematic testing, control-state reachability, and portability analysis, with an emphasis on efficient encodings and automated reasoning techniques.
Weak Memory Models
I specialise in the verification of concurrent programs under weak memory semantics, particularly x86/TSO and related architectures. I have investigated the computational complexity of key verification tasks—such as testing, reachability, and portability—and developed SMT-based methods and tools that enable scalable automated verification under these models.