My background is in theoretical Computer Science. Between 2009 and 2011 I was a researcher in the Language Based Technology group at the Technical University of Denmark, Copenhagen. I worked on 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 interests are 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.
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.
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.
- Stochastic Abstraction of Programs: Towards Performance-Driven Development - Michael Smith. PhD Thesis, University of Edinburgh. 2010
- Semantics Directed Compiler Generation - Michael Smith. Part II Dissertation, University of Cambridge. 2005
Conference Papers - Peer Reviewed
- Visualisation for Stochastic Process Algebras: The Graphic Truth - Michael Smith and Stephen Gilmore. To appear in the 8th European Performance Evaluation Workshop (EPEW). 2011.
- Controlling Modelling Artifacts - Michael Smith, Flemming Nielson and Hanne Riis Nielson. To appear in Quantitative Evaluation of Systems (QEST) 2011.
- Compositional Abstractions for Long-Run Properties of Stochastic Systems - Michael Smith. To appear in Quantitative Evaluation of Systems (QEST) 2011.
- Compositional Abstraction of PEPA Models for Transient Analysis - Michael Smith. In proceedings of the 7th European Performance Engineering Workshop (EPEW). LNCS volume 6342, Springer-Verlag. Bertinoro, Italy, September 2010.
- Abstraction and Model Checking in the PEPA Plug-in for Eclipse - Michael Smith. In proceedings of Quantitative Evaluation of Systems (QEST) 2010. IEEE Press. Williamsburg, Virginia, September 2010.
- 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 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.
- Engineering with Logic: HOL Specification and Symbolic-Evaluation Testing for TCP Implementations - Steve Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith and Keith Wansbrough. In proceedings of Principles of Programming Languages (POPL) 2006, 2006.
- Rigorous Specification and Conformance Testing Techniques for Network Protocols, as Applied to TCP, UDP, and Sockets - Steve Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith and Keith Wansbrough. In proceedings of ACM Special Interest Group on Data Communications (SIGCOMM) 2005, 2005.
Conference Papers - Not Reviewed
- Abstraction and Model Checking in the Eclipse PEPA Plug-in - Michael Smith. In proceedings of Process Algebra and Stochastically Timed Activities (PASTA) 2009. Edinburgh, August 2009.
- Acitivity Based Abstraction of PEPA Models - Michael Smith. In proceedings of Process Algebra and Stochastically Timed Activities (PASTA) 2008. Edinburgh, July 2008.
- Stochastic Bounding of PEPA Models - Michael Smith. In proceedings of Process Algebra and Stochastically Timed Activities (PASTA) 2007. London, July 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.
Other Documents and Papers
- Semantics Directed Compiler Generation - Michael Smith. Extended Abstract. 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