Research
We entrust large parts of our daily lives to computer systems, and these systems require thorough verification to ensure their correctness. System vulnerabilities can lead to leakage of confidential information, loss of money, and (in the case of cyber-physical systems) may even threaten one's physical safety and security. Many such bugs have in fact been found in computing systems in recent years, ranging from security vulnerabilities (like Meltdown and Spectre) to network errors to concurrency bugs. Current verification processes have proven inadequate for catching these bugs, resulting in the release of flawed hardware and software.
My work focuses on addressing the challenge of creating correct computing systems through formal methods, including modelling, verification, and synthesis. Formal modelling involves developing formalisms for computing systems that are capable of capturing their behaviour effectively and efficiently. Verification using formal methods, meanwhile, provides strong correctness guarantees based on mathematical proofs, and is adept at catching hard-to-find bugs. Finally, formal synthesis can automatically generate correct models or implementations of systems from high-level correctness specifications. Specific subject areas in systems that my formal methods research is currently investigating include memory consistency, security, cache coherence, and emerging architectures. Some of these projects have already generated publications.