My research project
Persistent safety and security
This project aims to tackle the challenges inherent to persistent memory. Persistent memory is a new paradigm for memory, preserving its contents even after power loss. Maintaining consistency, ensuring that causally dependent information persists in the correct order, and guaranteeing that persistent data are not available to unauthorized parties (after the recovery from a system failure) are some main concerns regarding persistent memory. My work focuses on formally verifying the correctness of persistent memory systems.
My main research interest is formal verification for software engineering. My current research focuses on verifying concurrent programs under non-volatile/weak memory models. The topics I address in my PhD include program logics, weak memory models, persistency semantics, concurrent correctness of software transactional memory algorithms, and more.