Essentially I am interested in using formal methods in the production of correct software.
On the formal side I have worked with the construction of operational semantics for state and event based systems. This includes concurrent systems. My interests lie in the construction of transformations between operational semantics that preserve notions like correctness, non-determinism and causality.
Formality, to be of use, must be both understandable and usable. Consequently I am interested both in how visualizations of models scale as the problem size grows and how we might achieve push button correctness of automatically generated approximations.
- *Currently I am actively looking at:
- software to model and verify event based systems
- defining process semantics that includes both probabilistic and non deterministic choice
- Modeling artifacts use in Software Defined Networking
- How modern practices for writing high assurance software can be best transferred to an Industrial setting in New Zealand. This work is undertaken in collaboration with Gallagher