Proposer:
Suggested Supervisors:
Principal goal of the project:
Description:
Hardware can be mathematically verified to meet a
specification of its intended behaviour. Formal verification can
increase confidence that the hardware will behave reliably,
safely and securely in use. Both the implementation of the
hardware and its specification must be presented as mathematical
formulae (usually in a suitable logic) and the verification
problem represented as a theorem proving problem. Usually the
proofs are not deep, but are long and complicated. Machine
assistance is required reduce the tedium and error rate.
Verification of a typical piece of industrial hardware usually
requires a human user to guide an interactive theorem prover. It
can take months or even years and require hundreds or thousands
of interactions. The long time delays and high skill levels
required in formal verification have meant that this technology
has not been taken up by industry except in exceptional
circumstances.
Proof planning is a technique, developed at Edinburgh, for
guiding the search for a proof using a global outline. We have
studied the common patterns in inductive proofs, represented
these patterns in proof plans and used them sucessfully to guide
large numbers of proof attempts. Francisco Cantu, a PhD student
at Edinburgh, has applied proof planning to hardware verification
with some success. He has been able to prove many of the
verification theorems with no or little user interaction. Typical
development times are a few weeks to: study the hardware;
represent the specification and implementation in logical form;
and prove the theorem. The plans for the proofs are developed
automatically in a few minutes. So far, Francisco has applied
these to textbook examples of circuits, ranging from an n-bit
adder, via a multiplier, shifter and ALU to a complete
microprocessor: the Gordon computer.
The next step is to see if this promising start will scale up
to real hardware. We have several suppliers who have promised
example hardware designs. We also have contacts with Mike
Gordon's HOL project at the University of Cambridge. Our plan is
to interface our proof planner, CLAM, to guide the HOL
interactive theorem prover. HOL has been used for interactive
verification of a number of commercial pieces of hardware. These
would then become available as test examples for the project.
The PhD student will use CLAM to prove a number of
verification theorems. Comparisons will be made with similar
proos on rival systems to see if a significant reduction in
development time and skill levels can be achieved with proof
planning. It will be necessary to tune our proof planner to this
domain, eg developing new, domain specific, proof plans;
improving the efficiency of CLAM when faced with very large
proofs; developing techniques for interaction to patch failed
proof attempts. A start has already been made on this tuning, but
more will probably be required as more difficult problems are
attempted. Work is going on at Cambridge and other labs on the
translation from existing commercial specification languages into
the logical form required for automatic theorem proving. The
student will draw on, and possibly add to, this work.
Resources Required:
Degree of Difficulty:
Background Needed:
References: