Academic Work
I'm currently a third year PhD student at the Laboratory for Foundations of Computer Science, University of Edinburgh. My supervisor is Jane Hillston. I am funded by a Microsoft Research European Scholarship. I'm looking at performance analysis of real implementations of distributed systems - namely extracting stochastic models from source 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 Stochastic Process Algebra (and in particular, the process algebra PEPA), and modelling distributed systems. I am interested in the use of performance modelling methodologies in Software Engineering, and in the development of tools to enable developers to analyse performance properties of their code. I would roughly divide my current work into two aspects:
- Stochastic Model Extraction - I am concerned with automating the process of going from source code to performance model. See the QAPL and PASTA papers below, for more information.
- Model Simplification - I am interested in applying aggregation to large PEPA models, and most importantly, reasoning about the error involved when doing so. Currently, I am investigating the use of stochastic bounds, in conjunction with other approximate aggregations.
Publications
- Probabilistic Abstract Interpretation of Imperative Programs using Truncated Normal Distributions - Michael Smith. In proceedings of the 6th Workshop on Quantitative Aspects of Programming Languages (QAPL). Budapest, March 2008.
- Stochastic Bounding of PEPA Models - Michael Smith. In proceedings of Process Algebra and Stochastically Timed Activities (PASTA) 2007. London, July 2007.
- Stochastic Modelling of Communication Protocols from Source Code - Michael Smith. In proceedings of the 5th Workshop on Quantitative Aspects of Programming Languages (QAPL). Braga, April 2007.
- Towards Stochastic Model Extraction: Performance Evaluation, Fresh from the Source - Michael Smith. In proceedings of Process Algebra and Stochastically Timed Activities (PASTA) 2006. London, June 2006.
Papers in Submission
Other Documents and Papers
- Semantics Directed Compiler Generation - Michael Smith. Extended Abstract. 2005
- Semantics Directed Compiler Generation - Michael Smith. Part II Dissertation. 2005
- PhD Research Proposal: Statistical Abstraction of Programs - Michael Smith. 2005
- Flow Control in the Linux Network Stack - Michael Smith, Steve Bishop. Tech Report. 2004
Revision Notes and Miscellany