Toby is a faculty member of the School of Computing and Information Systems. His research focuses on how to build highly secure computer systems using rigorous techniques, such as formal software verification and novel programming languages.

His recent accomplishments include co-developing the SecC program verifier for proving the security of concurrent C programs, leading the team that carried out the first proof of security for a non-trivial concurrent program, and the development of the award-winning Cross Domain Desktop Compositor.
Before joining the University of Melbourne, he worked at NICTA (now Data61) where he led the team that completed the world’s first proof that a general purpose operating system kernel could enforce data confidentiality, for the seL4 kernel; played a leading role in the development of the COGENT programming language for verified systems programming; and collaborated with DST Group to build and verify the security of seL4-based cross domain devices. He holds a D.Phil. in Computer Science from the University of Oxford, awarded in June 2011, and a Bachelor of Computer Science with First Class Honours from the University of Adelaide, awarded in August 2005.