I worked with the NICTA Trustworthy Filesystems team over the summer exporting type-correctness certificates & verifying transformations between the intermediate representations of programs in a linearly typed, restrictive DSL.
I'm currently working on my honours thesis, a variant of SIMPL with concurrent semantics to enable practical formal verification of concurrent C programs.
BSc Computer Science (UNSW, 2014)
Recognition and Awards
NICTA Summer Scholar Prize 2014-2015
|Sidney Amani, June Andronick, Maksym Bortin, Corey Lewis, Christine Rizkallah and Joseph Tuong|
COMPLX: A verification framework for concurrent imperative programs
International Conference on Certified Programs and Proofs, pp. 138–150, Paris, France, January, 2017
|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