Principal Researcher; Associate Professor, UNSW
Programming Languages Type Systems Domain specific languages Parallel Computing GPGPU
|Christine Rizkallah, Japheth Lim, Yutaka Nagashima, Thomas Sewell, Zilin Chen, Liam O'Connor, Toby Murray, Gabriele Keller and Gerwin Klein|
A framework for the automatic formal verification of refinement from Cogent to C
International Conference on Interactive Theorem Proving, Nancy, France, August, 2016
|Sidney Amani, Alex Hixon, Zilin Chen, Christine Rizkallah, Peter Chubb, Liam O'Connor, Joel Beeren, Yutaka Nagashima, Japheth Lim, Thomas Sewell, Joseph Tuong, Gabriele Keller, Toby Murray, Gerwin Klein and Gernot Heiser|
Cogent: verifying high-assurance file system implementations
International Conference on Architectural Support for Programming Languages and Operating Systems, pp. 175-188, Atlanta, GA, USA, April, 2016
|Liam O'Connor-Davis, Gabriele Keller, Sidney Amani, Toby Murray, Gerwin Klein, Zilin Chen and Christine Rizkallah|
CDSL version 1: Simplifying verification with linear types
Technical Report, NICTA, October, 2014
||Gabriele Keller, Toby Murray, Sidney Amani, Liam O'Connor-Davis, Zilin Chen, Leonid Ryzhyk, Gerwin Klein and Gernot Heiser|
File systems deserve verification too!
Workshop on Programming Languages and Operating Systems (PLOS), pp. 1-7, Farmington, Pennsylvania, USA, November, 2013
A revised version of this paper was published in Operating Systems Review, Volume 48, Issue 1, January 2014, pages 58-64.