My interests are broadly in the area of concurrency.
In recent years I have become interested in concurrent programming, particularly lock-free concurrent datatypes, and ways of analysing them:
- I have developed a concurrent lock-free binomial heap, and argued for its correctness.
- I have investigated how to test concurrent datatypes for linearizability.
- I have investigated how to analyse lock-free code using the process algebra CSP and its model checker FDR; I have used these techniques to analyse a lock-free queue, and to discover the cause of a deadlock in a channel implementation.
I am also interested in verification, particularly of concurrent systems, using model checking techniques.
- I have recently extended the technique of view abstraction, which can be used to verify systems with an unbounded number of similar components. In particular, I extended the technique to include components with an identity, where these identities could be passed between processes. I showed how to use these techniques to analyse concurrent datatypes based on linked lists.
- I have (with Tom Gibson-Robinson) extended the model checker FDR to include symmetry reduction.
- I have investigated parallel versions of Tarjan's Algorithm for finding loops or strongly connected components in a graph. This has various applications in model checking.
Previously I did a lot of work in the formal modelling and analysis of computer security.
Testing for Linearizability
In Concurrency and Computation: Practice and Experience. Vol. 29. No. 4. 2017.
Analysing Lock−Free Linearizable Datatypes Using CSP
In Thomas Gibson−Robinson‚ Philippa Hopcroft and Ranko ́Lazic, editors, Concurrency‚ Security and Puzzles: Essays Dedicated to Andrew William Roscoe on the Occasion of His 60th Birthday. Vol. 10160 of LNCS. Springer. 2017.
Models for CSP with availability information
In Mathematical Structures in Computer Science. Vol. 26. No. 6. Pages 1022–1053. 2016.