Dr. Liam O’Connor, Foundations Cluster, School of Computing, Australian National University.

We are looking for PhD students to join me working on topics related to programming languages and formal methods. This is a fully-funded scholarship for a PhD degree at the Australian National University, including a living stipend. Details on the scholarship and formal eligibility criteria are found here. Information about the ANU for postgraduate research can be found here.

The exact topic can be determined with the candidate, but we are particularly interested in topics in two themes: Semantic Foundations for Software Engineering, and Lightweight Formal Methods for Programming. Details of each theme are provided below.

Note that is not a prescription, and candidates wanting to pursue topics in other areas will also be considered. If you are interested in projects with both a strong theoretical component as well as real-world practical impact, please get in touch.

To express interest, please email me at this domain or via liam.oconnor at anu.edu.au. Please include details about yourself such as a CV. Formal applications are via the ANU portal (see the instructions) but applicants are encouraged to contact me informally first.

Semantic Foundations for Software Engineering

Description

Software Engineering abounds with tools and languages for specification, modelling, implementation, monitoring, analysis, verification and testing of software systems. These tools, however, are rarely backed up by formal semantics. Formalising the semantics of such artefacts has a number of benefits, including:

• Gaining a greater understanding of the meaning of these tools and languages, and how they relate to the software system they concern;
• Providing the groundwork for formal verification of these tools, giving mathematical proofs of the soundness and completeness of these tools, ensuring software safety, liveness and cybersecurity properties;
• Developing insight for the design of new tools and languages amenable to formal treatment.

As software systems become pervasive, the cost of critical bugs and vulnerabilities increases. This has led to a renewed interest in formal guarantees. Developing semantics for such systems is therefore of crucial importance for the development of future software with a high level of assurance.

Required Skills

A PhD in this area is necessarily quite mathematical, so applicants should be comfortable with discrete mathematics (logic, sets and proofs). Other mathematical topics that may be useful include topology, lattice theory, induction and coinduction, model theory, proof theory, category theory, abstract algebra and mathematical foundations, but familiarity with these is not required.

Essential programming skills and knowledge of algorithms and data structures is also required. In addition, experience in the following areas of computer science is useful, but not required: proof assistants (Lean, Coq, Isabelle/HOL, Agda, etc.), automata theory, computability theory, domain theory, programming languages theory (e.g. operational semantics, types), concurrency theory, functional programming, formal verification.

Prior Work

In recent years I have been working with my PhD student Rayhana Amjad to develop semantics for Linear Temporal Logic variants used in runtime verification, monitoring, and testing:

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), Calgary, Canada, 2024.
Electronic Proceedings in Theoretical Computer Science, to appear.

Another relevant project, now completed, is Shoggoth, which is the first comprehensive accounting of the semantics of strategic rewriting languages, commonly (but not exclusively) used in particular for the design and modelling of compiler optimisations. This work was part of the PhD project of Dr. Xueying Qin.

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

Lightweight Formal Methods for Programming

Description

In recent years, the success of projects like seL4, CompCert and Cogent suggest that achieving end-to-end mathematical guarantees of safety and security are not out of reach for foundational software systems, and yet the vast majority of software is developed without such guarantees. The reason is simple: insisting on full, end-to-end formal guarantees of correctness produces projects that are more costly, require greater expertise to develop, and take more time than traditional low-assurance software development. Yet, in the world of formal methods there exist specification languages, automatic analyses, models and systems that can be put to use in low-cost scenarios. These methods improve the reliability of software without dramatically increasing costs.

Examples of such lightweight formal methods include property-based testing, first pioneered in the Haskell QuickCheck library, where software systems are tested based on formal (usually algebraic) specifications. Now property-based testing libraries exist for all common programming languages and it enjoys widespread industrial use.

Another example is type systems, arguably the most widely-deployed instance of formal methods in software engineering. Type systems typically ensure type and memory safety properties, but they can be extended with all kinds of analyses to enable developers to couple specifications to their implementations and have them automatically checked by the compiler. At the extreme end of this, with liquid and dependent type systems, full correctness can be verified using type system techniques.

Topics in this theme would revolve around taking techniques established in the formal methods community and applying them to practical software engineering tools and programming languages.

Required Skills

Applicants in this theme will need strong programming skills, including skill at algorithms and data structures. Experience in Software Engineering is positive. Other computer science areas that are useful for this theme include: automata theory, type systems and programming languages, compilers, software modelling, formal verification, software specification, theorem proving. Mathematical maturity, particularly in discrete mathematics, is also a plus.

Prior Work

Three projects of mine come to mind for this theme. The first, Quickstrom, is a property-based testing tool which enables acceptance testing of web applications using a testing variant of Linear Temporal Logic called QuickLTL. This project is joint work with Oskar Wickström.

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

Another project in this theme is Dargent, an extension to my Cogent language for systems verification, that enables automatic verification of data layouts in memory:

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

Another extension to Cogent was integrating it with property-based testing, also relevant to this theme:

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