Scheme: Wolfson Research Merit Awards
Organisation: Queen Mary, University of London
Dates: Oct 2007-Mar 2012
Summary: I have been focussed on two problems.
The first is how we can deal with many computer processes running at the same time. The basic difficulty can be seen by analogy. The need for speed drives chip designers to try to make something akinto a super-motorwayfor thousands of vehicles speeding along side-by-side, but with no clearly demarcated lanes. With so many vehicles hurtling around at great pace, there becomes all the more danger of accidents. It is similar with computers. Different processes running at the same time can race with one another, and end up corrupting each other's data. But, chip designers are giving us more and more processors on one chip, leading to greater danger for the programmer, and greater fun for the scientist. The fun comes from trying to figure out how to make sense of the potential mayhem. My favoured approach uses formal logic -- the theory of reasoning -- as a way to make sure that all the processes behave safely, while maximising speed.
The second problem concerns how we can gather some information on how an unknown piece of code works, without running it. The approach I have been taking with several colleagues borrows a page out of the philosophy of science. We view a big piece of software, like an operating system, as if it was given to us from nature. It might me man-made, but it has probably evolved unpredictably over a number of years as various people worked on the code. Instead of inquiring into the motivation of the designer, we take a scientific point of view: the code is like data (like the human genome), and we want to dig information out of it. We do this using an idea called abductive inference, which is reasoning that identifies hypotheses that support conclusions. Scientists do abduction all the time, and we have a software too that does some of it too. Our tool, Abductor, automatically finds hypotheses that are needed for portions of code to run without error. It seems to open up a lot of new possibilities.