Static analysis of device drivers: we can do better! - Sidney Amani; Leonid Ryzhyk; Alastair F. Donaldson; Gernot Heiser; Alexander Legg; Yanjin Zhu (APSys, 2011)

Automatic Verification of Message-Based Device Drivers - Sidney Amani; Peter Chubb; Alastair F. Donaldson; Alexander Legg; Leonid Ryzhyk; Yanjin Zhu (SSV, 2012)

Automatic verification of active device drivers. - Sidney Amani; Peter Chubb; Alastair F. Donaldson; Alexander Legg; Keng Chai Ong; Leonid Ryzhyk; Yanjin Zhu (ACM SIGOPS Oper. Syst. Rev., 2014)

File systems deserve verification too! - Gabriele Keller; Toby C. Murray; Sidney Amani; Liam O'Connor; Zilin Chen; Leonid Ryzhyk; Gerwin Klein; Gernot Heiser (ACM SIGOPS Oper. Syst. Rev., 2014)

Specifying a Realistic File System. - Sidney Amani; Toby C. Murray (MARS, 2015)

CoGENT: Verifying High-Assurance File System Implementations. - 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; et al. (ASPLOS, 2016)

Refinement through restraint: bringing down the cost of verification. - Liam O'Connor; Zilin Chen; Christine Rizkallah; Sidney Amani; Japheth Lim; Toby C. Murray; Yutaka Nagashima; Thomas Sewell; Gerwin Klein (ICFP, 2016)

COMPLX: A Verification Framework for Concurrent Imperative Programs. - Sidney Amani; June Andronick; Maksym Bortin; Corey Lewis; Christine Rizkallah; Joseph Tuong (Arch. Formal Proofs, 2016)

COGENT: Certified Compilation for a Functional Systems Language. - Liam O'Connor; Christine Rizkallah; Zilin Chen; Sidney Amani; Japheth Lim; Yutaka Nagashima; Thomas Sewell; Alex Hixon; Gabriele Keller; Toby C. Murray; Gerwin Klein (CoRR, 2016)

A methodology for trustworthy file systems. - Sidney Amani (2016)

Towards verifying ethereum smart contract bytecode in Isabelle/HOL. - Sidney Amani; Myriam Bégel; Maksym Bortin; Mark Staples (CPP, 2018)

Cogent: uniqueness types and certifying compilation. - Liam O'Connor; Zilin Chen; Christine Rizkallah; Vincent Jackson; Sidney Amani; Gerwin Klein; Toby Murray; Thomas Sewell; Gabriele Keller (J. Funct. Program., 2021)