My research topics to date have been functional programming languages (in particular, methods of
implementing IO) and model checking of Petri Nets (in particular, *compositional* reachability
checking).

**Compositional model checking of Petri Nets**:

My PhD research focussed on compositionally checking reachability in systems modeled by Petri nets.

*Compositional Reachability in Petri Nets*, Reachability Problems '14with Julian Rathke and Paweł Sobociński, paper (PDF)

- A divide-and-conquer algorithm for a modified version of the reachability/coverability problem in 1-bounded Petri nets that relies on the compositional algebra of nets with boundaries. We consider the algebraic decomposition of the net of interest as part of the input, allowing our technique to exploit modern techniques for NFA minimisation and equivalence checking, giving impressive scalable performance to systems with many (repeated) components. We formally prove our technique correct and demonstrate the scalable performance of our implementation by contrasting with existing state-of-the-art tools that exploit partial order reduction techniques on the global net.

*A Programming Language for Spatial Distribution of Net Systems*, Petri Nets '14with Paweł Sobociński, paper (PDF)

- Petri nets famously expose concurrency directly in their statespace. Building on the work on the compositional algebra of nets with boundaries, we show how an algebraic decomposition allows one to expose both concurrency and spatial distribution in the statespace. We introduce a simple domain specific language (DSL), PNBml, for the construction of nets in terms of their components, using PNBml to express several well-known parametric examples.

*Penrose: Putting Compositionality to Work for Petri Net Reachability*, CALCO'13with Paweł Sobociński, paper (PDF)

- We outline a novel technique for reachability checking in Petri Nets, exploiting compositionality to increase performance for some well-known examples. We introduce a tool that uses this technique, Penrose, discuss some design details in its implementation.

**IO in functional programming languages**:

My masters research project investigated methods of implementing input/output (I/O) in functional programming languages: report (PDF).