Quickstrom and LTL Testing
A project with Oskar Wickström bringing the power of property-based testing to web application interface testing. More information is available at the Quickstrom website. This section also includes broader theoretical investigations into testing for linear temporal logics and related topics.
Liam O'Connor, Oskar Wickström
Quickstrom: Property-based Acceptance Testing with LTL
Specifications
Programming Languages Design and Implementation (PLDI), pp.
1025-1038, San Diego, California, USA, June 2022.
Available from arXiv Talk available on
YouTube
Rayhana Amjad, Rob van Glabbeek, Liam O'Connor
Semantics for Linear-time Temporal Logic with Finite
Observations Expressiveness in Concurrency and Structural
Operational Semantics (EXPRESS/SOS), pp. 35-50, Calgary, Canada,
September 2024
Available
from ETPCS Proofs on
AFP
Cogent
A project at the Trustworthy Systems Group aimed at using programming languages with interesting types to aid verification of low-level systems. More information is available at the Cogent website.
Zilin Chen, Ambroise Lafont, Liam O'Connor, Gabriele Keller, Craig
McLaughlin, Vincent Jackson, Christine Rizkallah
Dargent: A Silver Bullet for Verified Data Layout
Refinement
Principles of Programming Languages (POPL), Boston,
Massachusetts, USA, 2023.
Proceedings of the ACM on Programming Languages, Volume 7, January 2023,
Article 47, pp 1369–1395
Available
from TS Talk
available on YouTube
Zilin Chen, Christine Rizkallah, Liam O'Connor, Partha Susarla,
Gerwin Klein, Gernot Heiser, Gabriele Keller
Property-Based Testing: Climbing the Stairway to
Verification
Software Language Engineering (SLE), pp. 84-97, Auckland, New
Zealand, December 2022.
Winner of Distinguished Artifact Award.
Available
from TS
Louis Cheung, Liam O'Connor, Christine Rizkallah
Overcoming Restraint: Composing Verification of Foreign
Functions with Cogent
Certified Programs and Proofs (CPP), pp. 13-26, Philadelphia,
Pennsylvania, USA, January 2022.
Available from arXiv Talk available on
YouTube
Liam O'Connor, Zilin Chen, Christine Rizkallah, Vincent Jackson,
Sidney Amani, Gerwin Klein, Toby Murray, Thomas Sewell, Gabriele
Keller
Cogent: Uniqueness types and Certifying
Compilation
Journal of Functional Programming, Volume 31, Issue on Secure
Compilation, October 2021.
Available
from CUP
Liam O'Connor
Type Systems for Systems Types
PhD Thesis, Computer Science and Engineering, Faculty of
Engineering, University of New South Wales, 2019
Available
from UNSWorks
Liam O'Connor, Zilin Chen, Partha Susarla, Christine Rizkallah,
Gerwin Klein, Gabriele Keller
Bringing effortless refinement of data layouts to
Cogent
International Symposium On Leveraging Applications of Formal
Methods, Verification and Validation (ISOLA), LNCS v. 11244, pp.
134-149, Limassol, Cyprus, November, 2018
Available
from TS
Gerwin Klein, June Andronick, Gabriele Keller, Daniel Matichuk, Toby
Murray, Liam O'Connor
Provably Trustworthy Systems
Philosophical Transactions of the Royal Society A, Volume 375, Issue
2104.
Available
from the Royal Society
Zilin Chen, Liam O'Connor, Gabriele Keller, Gerwin Klein and Gernot
Heiser
The Cogent Case for Property-Based Testing
Workshop on Programming Languages and Operating Systems (PLOS), pp.
1-7, Shanghai, China, October, 2017
Available
from TS
Liam O'Connor, Zilin Chen, Christine Rizkallah, Sidney Amani, Japheth
Lim, Toby Murray, Yutaka Nagashima, Thomas Sewell, Gerwin Klein
Refinement through Restraint: Bringing Down the Cost of
Verification
International Conference on Functional Programming (ICFP), pp.
89-102, Nara, Japan, September 2016.
Available
from TS Talk
available on YouTube
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 (ITP),
LNCS v. 9087, pp. 323-340, Nancy, France, August 2016.
Available
from TS
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 (ASPLOS), pp. 175-188, Atlanta, GA,
USA, April 2016.
Available
from TS
Liam O'Connor, 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.
Available
from TS
Gabriele Keller, Toby Murray, Sidney Amani, Liam O'Connor, 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.
Available
from TS
Dependent types and type systems
Liam O'Connor
Deferring the Details and Deriving Programs
Workshop on Type-Driven Development (TyDe), pp. 27-39, Berlin,
Germany, August, 2019.
Available here Talk available on
YouTube
Liam O'Connor
Applications of Applicative Proof Search
Workshop on Type-Driven Development (TyDe), pp. 43-55, Nara,
Japan, September, 2016.
Available here Talk available on
YouTube
Liam O'Connor
Formalising GHC's Type System
Undergraduate Thesis, UNSW, 2012.
Available here
Miscellaneous
Xueying Qin, Liam O'Connor, Rob van Glabbeek, Peter Höfner, Ohad
Kammar and Michel Steuwer
Shoggoth: A Formal Foundation for Strategic
Rewriting
Principles of Programming Languages (POPL), London, UK,
2024.
Proceedings of the ACM on Programming Languages, Volume 8, January 2024,
Article 3, pp 61–89
Available from
ACM
Xueying Qin, Liam O'Connor and Michel Steuwer
Primrose: Selecting Container Data Types by Their
Properties
The Art, Science, and Engineering of Programming, Vol. 7, Issue
3, Article 11, 2023
Available from
‹Programming›
Liam O'Connor and Rayhana Amjad
Holbert: Reading, Writing, Proving and Learning in the
Browser
Human Aspects of Types and Reasoning Assistants (HATRA),
Auckland, New Zealand, 2022.
Live Version Here Available on arXiv Talk available on
YouTube
Yutaka Nagashima and Liam O'Connor
Close Encounters of the Higher Kind: Emulating Constructor
Classes in Standard ML
Workshop on ML 2016, Nara, Japan, September, 2016.
Available
from TS Talk
available on YouTube
Liam O'Connor
Gentzen: A Beginner's Proof Assistant based on Higher Order
Logic
Undergraduate Project, UNSW, 2012
Available here