"You're my wife now!" -- Papa Lazarou, The League Of Gentlemen

Academic Work

I'm a theoretical Computer Scientist in the Language Based Technology group at the Technical University of Denmark, Copenhagen. I'm employed by the MT-LAB project, which is a collaboration between DTU, Aalborg University, and ITU, investigating formal verification techniques for advanced software systems. My particular research is concerned with probabilistic and stochastic analysis of distributed systems.

Before this, I was a PhD student at the Laboratory for Foundations of Computer Science, University of Edinburgh. My supervisor was Professor Jane Hillston, and I was funded by a Microsoft Research European Scholarship. My thesis was concerned with performance analysis of real implementations of distributed systems - namely, extracting stochastic models from program code (see here for more information).

In 2005, I graduated with 1st class honors in Computer Science from Robinson College, Cambridge. I was awarded the Microsoft Research Prize for Best Student, and shortlisted for the S.E.T. Award for Information Technology Student of the Year. Before Cambridge, I attended Headlands School, in Bridlington, where I took my GCSE and A-Level exams.

In the summer of 2005 I was a Senior Technical Associate at Fraser Research, in Princeton, New Jersey. Working with Sandy Fraser, I developed and simulated algorithms for fast restoration in large-scale broadband access networks, based on actively-switched components with redundant links. I also worked with John Billings on a preliminary study of naming semantics for the Internet.

My final year project was a semantics directed compiler generator, for which I was awarded a Data Connection Prize for Outstanding Dissertation. SemCom is an interpreter generator for arbitrary languages, based on a two-level natural semantics style definition. The metalanguage SDL allows specification of type systems up to polymorphism, and the execution engine is general enough to allow small-step dynamic semantics as well. Numerous analyses are performed to transform the semantics (including sequentialisation of premises and conditions) and provide consistency checks, and a lexer and parser are automatically generated from the semantics.

In the summer of 2004, I worked as an intern on the Netsem project (headed by Peter Sewell), which is in the late stages of developing a post-hoc operational (LTS-style) semantics of TCP.

Research Interests

My research revolves around performance analysis of software, and in particular I'm interested in the application of two formal verification techniques. The first is static analysis which is about developing techniques for analysing software without having to run it. I'm looking at how these techniques can be extended to deal with quantitative aspects of software, such as performance. The second technique is model checking, and more specifically, stochastic model checking. Here, we construct a model of the system - often in a an abstract formalism such as a stochastic process algebra (e.g. PEPA) - and then specify properties of the system in an appropriate logic. I'm particularly interested in developing abstractions that enable us to analyse really large models.

I'm interested in both the theoretical and the practical aspects of these techniques, and in particular I want to make it easier for developers to build distributed software systems in a performance-driven way.

Publications

Papers in Submission

Other Documents and Papers

Revision Notes and Miscellany