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 University of Surrey and a member of the Surrey 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.