Dr. Liam O’Connor, Laboratory for Foundations of Computer Science, University of Edinburgh, Scotland.

We are looking for a PhD student to join me working on topics related to programming languages and formal methods. This is a fully-funded scholarship for 3.5 years here at Edinburgh, with the intention to start in September 2022 or possibly January of 2023.

The exact topic can be determined with the candidate, but we are particularly interested in topics related to the Quickstrom project, detailed below.

The candidate should ideally have some experience with formal methods, particularly algorithmic verification, or some other closely-related area such as functional programming, theorem proving, software engineering, programming language semantics or property-based testing. Note that is not an exclusive list, and candidates from 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. Please include details about yourself such as a CV.

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 of Monoid Consulting, and already enjoys industry use. Possible topics may include one or more of the following themes:

• Extending Quickstrom with techniques from model inference (such as automata learning) and model checking (such as abstraction-refinement), or targeted testing based on search techniques, to improve on randomly generated tests.
• Extensions to Quickstrom’s logic and implementation to accommodate security properties and hyperproperties.
• Integration of Quickstrom with more powerful verification tools.
• Metatheoretical results to position QuickLTL with respect to other temporal logics, including extensions to security.