About me
Rob is a postdoc at UNSW Sydney who researches and develops formal methods, primarily for proving absences of information flow in systems for high-assurance use cases. In the past, their focus was on complications arising from concurrency and refinement to enable secure compilation; more recently, it has been on how to prove an OS enforces absences of information leaks through the microarchitecture. More broadly, they are interested in all applications of interactive theorem proving, as well as anything to do with the design and construction of software systems with formally proved correctness and security properties at scale.