I am employed on the PROWESS project, which is applying Property Based Testing techniques to Erlang and distributed, concurrent systems. My work has focused on test adequacy measures. I have created Smother, which generates MC/DC style analysis for Erlang code, and mu2, which is a mutation testing framework for Erlang. I have also written Synapse as an interface between Erlang testing tools and Model Inference tools (e.g. StateChum)
I have been working with Kirill on the StateChum system. StateChum is a grammar inference system that takes program traces and uses language learning algorithms to infer a Finite State Machine representation of the program's behaviour. One of the learning algorithms - QSM - takes the information it is presented and then asks questions of an expert oracle to expand its understanding and refine the FSM. I have been working on wrapper and interface frameworks for Erlang modules that can use the System Under Test as the oracle for these questions, so the questions are answered by running dynamic tests on the SUT with a forced trace.
After graduating from The University of Kent I spent several years working for DSTL in safety critical systems. In that time I saw a large number of projects that applied serious formal verification techniques to serious software. As well as the range of test case management techniques and hazard mitigating safety cases I worked on projects that used a selection of language formalisations to allow static analysis. The two major examples are SPARK Ada and MISRA C. In both cases they work by limiting the original languages (Ada and C) to only those features whose operation can be entirely determined without any knowledge of the compiler's behaviour or the state of the underlying hardware. This is an effective way of producing high integrity code; even where it seems to add extra hassle for programmers by removing their favourite operator for doing everything in one go, it forces them to think more carefully about the problem they are solving and the possible failure conditions.
Since these approaches work by abstracting away the compiler and underlying hardware there is one area that is - by definition - excluded: software that interacts directly and intentionally with hardware (e.g. device drivers).
I am interested in producing formal models of programs whose behaviour depends on details of the hardware on which they run, and where the program's specification includes specific hardware interactions. Device drivers are an obvious example.
Spurinna, the prototype system developed during my PhD is available here.