Gavin Lowe
Gavin Lowe
Wolfson Building, Parks Road, Oxford OX1 3QD
Interests
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.
See also
Selected Publications
-
Testing for Linearizability
Gavin Lowe
In Concurrency and Computation: Practice and Experience. Vol. 29. No. 4. 2017.
Details about Testing for Linearizability | BibTeX data for Testing for Linearizability
-
Analysing Lock−Free Linearizable Datatypes Using CSP
Gavin Lowe
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.
Details about Analysing Lock−Free Linearizable Datatypes Using CSP | BibTeX data for Analysing Lock−Free Linearizable Datatypes Using CSP
-
Models for CSP with availability information
Gavin Lowe
In Mathematical Structures in Computer Science. Vol. 26. No. 6. Pages 1022–1053. 2016.
Details about Models for CSP with availability information | BibTeX data for Models for CSP with availability information