# Abstraction Discovery and Refinement for Model Checking Partially Ordered State Spaces

1st October 2006 to 31st March 2010

Integrated electronic chips, such as the processor in your laptop, are among the most complex artifacts ever devised by humans.
They consist of many millions of interconnected transistors, all working together to run programs. The engineering design
of these chips is extremely challenging, and very difficult to get right. Checking that a modern electronics design will produce
a chip that does what it's supposed to do occupies up to 80% of the effort in designing a new chip and requires months or
years of computer simulation using large banks of computers. Formal verification is an approach to this problem that aims
to improve the quality of chip designs using logical reasoning instead of simulation. A mathematical model of the chip design
is constructed, and mathematical proofs are done to show that the model describes just those behaviours that we wish the chip
itself to have. These models and proofs are usually very complex - far too big for pencil-and-paper mathematics - and specialised
computer software is used for them. With formal verification, the functioning of a chip can often be tested and errors discovered
far more thoroughly and with much less effort than by simulating it. But there is a problem with this approach too: an accurate
and fully detailed mathematical model of a modern chip design would itself be vastly too large and complex to represent and
do proofs about, even using state of the art software. An approach to solving this problem is to let the mathematical models
we use be abstractions, or simplifications, of the chip designs they represent. Instead of modelling the design in full detail,
we represent only its salient features - only those aspects of it which, if got wrong, will produce an error. An abstract
model can be much smaller than a fully detailed one, and so be much easier to handle. The difficulty with this method is coming
up with an appropriate abstraction. If the abstraction throws away too much information about the design, then it may not
say enough about its behaviour to establish that the design does the expected thing. Even worse, such an oversimplification
may give a false assurance that the design is right. On the other hand, if we retain too much information about the design,
then the model may be too big to be tractable. The problem of finding a good abstraction in general is very difficult and
in practice often requires a great deal of human ingenuity and insight. It would be much better to have a way to find good
abstractions automatically. One idea is to begin with a fairly crude abstraction, one that simplifies a great deal. If doing
proofs with this reveals an error, then we check if there really is an error in the actual design, or if the problem is just
an artefact of oversimplification in our model. (There are ways to check this efficiently.) If the error is real, we have
found a problem with our design and can repair it. If the error is spurious, then it can give us information that will allow
us to refine our abstraction by adding more of the right kind of design detail to it to get a more accurate one. Repeating
this process arrives, we hope, at a tractable abstraction that is sufficient for checking our design. This basic idea has
many variants and technical subtleties, and there is a rich literature of advanced research on this topic. This project at
Oxford will make a contribution to this research by looking at ways of constructing abstractions in a specific modelling and
proof framework called Symbolic Trajectory Evaluation (STE). This is one of the most practical formal verification methods;
it is used, for example, by Intel. STE provides an especially rich setting for abstractions, but so far most abstractions
in STE have been created manually - by experts and with much effort. This research will develop a new abstraction refinement
method for STE that will exploit its full potential and make it much easier forengineers to use effectively.