I am currently reading for a Ph.D. in the Foundations of Computer Science at the University of Edinburgh, Scotland. I began my scholarship in October 2010 and I am a member of the Laboratory for Foundations of Computer Science (LFCS) at Edinburgh. I am funded by an EPSRC scholarship. I received an M.Sc. in Theoretical Computer Science from the University of Edinburgh in 2010 and, previously, I received a B.Sc. in Software Engineering from the University of Manchester in 2008. I occasionally work as a consultant software engineer and a freelance photographer.
My academic interests (broadly) include:
My research is concerned with the development of a temporal logic and model checking algorithms for the continuous π-calculus. My supervisor is Ian Stark and my work continues the work of Marek Kwiatkowski.
The continuous π-calculus (cπ) is a process algebra with a compositional, continuous time and continuous space semantics in terms of real vector spaces. The ability to model a continuous state-space of real values is especially useful in the modelling of biochemical systems where the state of the system is described in terms of the real valued concentrations of chemical species. The project aims to augment the existing cπ theory with a means to perform model checking on cπ models. That is, the mechanical verification that some formal logical assertion holds for the model. A logic equipped with a notion of real numbers will need to be developed, suitable for making assertions about a continuous state space along with an algorithm for verification of these assertions.
I am developing a logic - which can be seen as a formal query langauge - for expressing behavioural properties of cπ models. The logic of behvaiour in context (LBC) is a time bounded temporal logic extended with a modality which allows things (i.e. new chemical species) to be introduced to the model. This allows the expression of properties of the behaviour when species are introduced to the model over time.
Some of this is described in more detail (with pictures) on this poster
My M.Sc. thesis was on model checking the independence-friendly modal μ-calculus. Independence-friendly logic is an extension of first order logic which allows the expression of independence between quantifiers. IF logic potentially has applications in the verification of concurrent computer systems. However, even the smallest examples are so complex that they are almost impossible to do by hand. My project centred on the implementation of a model checker which checked models of concurrent systems (in CCS) against specifications expressed in a version of the modal μ-calculus which has been extended to express IF modalities. My M.Sc. supervisor was Julian Bradfield. See his research page for more information on IF logic and the modal μ-calculus.
I am originally from Formby, near Liverpool, England. I lived in Manchester for some time and I now live in Edinburgh, Scotland (after a brief period in Falkirk). In my spare time I can usually be found climbing mountains, cycling, taking photographs (I have also worked as a freelance sports photographer), reading, tinkering with computer systems, cooking, playing strategy games (board and computer), enjoying fine British ales in fine British pubs or brewing my own.
I am one of a number of students, research and academic staff at the University of Edinburgh, School of Informatics who are producing a computer science podcast, CompuCast. We believe that CompuCast is the only periodical digital media publication of its kind. CompuCast aims to provide monthly, topical discussions of the news and latest research in computer science. We also present features about topics of interest to fellow computer scientists, interviews with field leading researchers, as well as some more light-hearted and fun topics.
More information and episodes to download can be found on our website at computersciencepodcast.com
We would be keen to hear from anyone who might be interested in contributing to the podcast. Maybe if anyone is visiting Edinburgh and would like to come to chat with us, or if anyone would like to record any features to send to us, please get i