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)

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)

Applications of applicative proof search. - Liam O'Connor (TyDe@ICFP, 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)

A Framework for the Automatic Formal Verification of Refinement from Cogent to C. - Christine Rizkallah; Japheth Lim; Yutaka Nagashima; Thomas Sewell; Zilin Chen; Liam O'Connor; Toby C. Murray; Gabriele Keller; Gerwin Klein (ITP, 2016)

Close Encounters of the Higher Kind Emulating Constructor Classes in Standard ML. - Yutaka Nagashima; Liam O'Connor (CoRR, 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)

The Cogent Case for Property-Based Testing. - Zilin Chen; Liam O'Connor; Gabriele Keller; Gerwin Klein; Gernot Heiser (PLOS@SOSP, 2017)

Bringing Effortless Refinement of Data Layouts to Cogent. - Liam O'Connor; Zilin Chen; Partha Susarla; Christine Rizkallah; Gerwin Klein; Gabriele Keller (ISoLA (1), 2018)

Deferring the details and deriving programs. - Liam O'Connor (TyDe@ICFP, 2019)

Type Systems for Systems Types. - Liam O'Connor (2019)

Overcoming Restraint: Modular Refinement using Cogent's Principled Foreign Function Interface. - Louis Cheung; Liam O'Connor; Christine Rizkallah (CoRR, 2021)

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)

Overcoming restraint: composing verification of foreign functions with cogent. - Louis Cheung; Liam O'Connor; Christine Rizkallah (CPP, 2022)

Quickstrom: property-based acceptance testing with LTL specifications. - Liam O'Connor; Oskar Wickström (PLDI, 2022)

Property-Based Testing: Climbing the Stairway to Verification. - Zilin Chen; Christine Rizkallah; Liam O'Connor; Partha Susarla; Gerwin Klein; Gernot Heiser; Gabriele Keller (SLE, 2022)

Holbert: Reading, Writing, Proving and Learning in the Browser. - Liam O'Connor; Rayhana Amjad (CoRR, 2022)

Dargent: A Silver Bullet for Verified Data Layout Refinement. - Zilin Chen; Ambroise Lafont; Liam O'Connor; Gabriele Keller; Craig McLaughlin; Vincent Jackson; Christine Rizkallah (Proc. ACM Program. Lang., 2023)

Primrose: Selecting Container Data Types by Their Properties. - Xueying Qin; Liam O'Connor; Michel Steuwer (Art Sci. Eng. Program., 2023)

Artifact for Shoggoth - A Formal Foundation for Strategic Rewriting. - Xueying Qin; Liam O'Connor; Rob van Glabbeek; Peter Höfner; Ohad Kammar; Michel Steuwer (Zenodo, 2023)

Artifact for Shoggoth - A Formal Foundation for Strategic Rewriting. - Xueying Qin; Liam O'Connor; Rob van Glabbeek; Peter Höfner; Ohad Kammar; Michel Steuwer (Zenodo, 2023)

Definitive Set Semantics for LTL3. - Rayhana Amjad; Rob van Glabbeek; Liam O'Connor (Arch. Formal Proofs, 2024)

Semantics for Linear-time Temporal Logic with Finite Observations. - Rayhana Amjad; Rob van Glabbeek; Liam O'Connor (EXPRESS/SOS, 2024)

Shoggoth: A Formal Foundation for Strategic Rewriting. - Xueying Qin; Liam O'Connor; Rob van Glabbeek; Peter Höfner; Ohad Kammar; Michel Steuwer (Proc. ACM Program. Lang., 2024)