Skip to main content

Sidney Amani

Sidney Amani
Research Engineer

Research Interests

Sidney's research focuses on finding a practical approach to make file systems amenable to a functional correctness proof formalised in an interactive theorem prover. His previous research includes developing a framework to automatically verify device drivers interactions with the rest of the operating system.

Contact Details

Phone: +61 2 9490 5866
Email:Sidney.Amani@data61.csiro.au

More contact information is available at the Contact page.

Photo of Sidney Amani

Publication List

Projects

Current

Past

Publications

Data61 Papers

2016

Abstract PDF Sidney Amani, June Andronick, Maksym Bortin, Corey Lewis, Rizkallah Christine and Joseph Tuong
Complx: A verification framework for concurrent imperative programs
International Conference on Certified Programs and Proofs, pp. 138-150, Paris, France, December, 2016
Abstract PDF Liam O'Connor, Zilin Chen, Christine Rizkallah, Sidney Amani, Japheth Lim, Toby Murray, Yutaka Nagashima, Thomas Sewell and Gerwin Klein
Refinement through restraint: Bringing down the cost of verification
International Conference on Functional Programming, Nara, Japan, September, 2016
Abstract PDF Sidney Amani
A methodology for trustworthy file systems
PhD Thesis, CSE, UNSW, Sydney, Australia, August, 2016

NICTA Papers

2016

Abstract PDF 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

2015

Abstract PDF Sidney Amani and Toby Murray
Specifying a realistic file system
Workshop on Models for Formal Analysis of Real Systems, pp. 1-9, Suva, Fiji, November, 2015

2014

Abstract PDF 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
Abstract PDF Sidney Amani, Peter Chubb, Alastair Donaldson, Alexander Legg, Keng Chai Ong, Leonid Ryzhyk and Yanjin Zhu
Automatic verification of active device drivers
ACM Operating Systems Review, Volume 48, Number 1, May, 2014

2013

Abstract PDF 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.

2012

Abstract PDF Sidney Amani, Peter Chubb, Alastair Donaldson, Alexander Legg, Leonid Ryzhyk and Yanjin Zhu
Automatic verification of message-based device drivers
Systems Software Verification, pp. 1–14, Sydney, Australia, November, 2012
Abstract PDF Sidney Amani, Peter Chubb, Alastair Donaldson, Alexander Legg, Leonid Ryzhyk and Yanjin Zhu
Active device drivers
Technical Report, NICTA, September, 2012
Abstract
Slides
PDF Sidney Amani, Leonid Ryzhyk and Toby Murray
Towards a fully verified file system
Poster presentation at EuroSys Doctoral Workshop, Bern, Switzerland, April, 2012

2011

Abstract PDF Sidney Amani, Leonid Ryzhyk, Alastair Donaldson, Gernot Heiser, Alexander Legg and Yanjin Zhu
Static analysis of device drivers: we can do better!
Asia-Pacific Workshop on Systems (APSys), pp. 1-5, Shanghai, China, July, 2011