Research Interests

My research interests lie in the development of automated reasoning techniques that support the construction of safe and secure software intensive systems – from requirements through to coding. Building scalable automated reasoning tools requires an integration of techniques. I am particularly interested in combining static (i.e. theorem proving) and dynamic analysis (i.e. animation and execution logs). I am interested in approaches where there is a strong cooperation between complementary techniques. That is, where individual techniques combine their strengthens, but crucially compensate for each other's weaknesses through the communication of partial results and failures. A recurring theme within my research is the productive use of failure – using the analysis of a failed proof attempt to automate the synthesis of creative steps, e.g. missing properties that are required in order to establish the correctness of a system. I see such automation as improving the creativity and productivity of an engineer. To promote accessibility, I seek where possible to embed my work within conventional tools and methodologies.

Keywords: automated reasoning; meta-level reasoning; formal modelling and refinement; verification and synthesis; productive use of failure; combining animation with theory formation; problem frames; combining informal and formal modelling; safety and security; embeded formal methods.

I am interested in supervising PhD, MSc and BSc projects in the broad areas described above.

Research Projects