%T Towards the Formal Verification of a Java Processor in Event\-B
%A  Neil Grant,  Neil Evans
%E  Alistair A. McEwan,  Steve Schneider,  Wilson Ifill, Peter H. Welch
%B Communicating Process Architectures 2007
%X Formal verification is becoming more and more important in
   the production
of high integrity microprocessors. The
   general purpose formal method called Event\-B is the latest
   incarnation of the B Method: it is a proof\-based approach
   with a formal notation and refinement technique for
   modelling and verifying systems. Refinement enables
   implementation\-level features to be proven correct with
   respect to an abstract specification of the system. In this
   paper we demonstrate an initial attempt to model and verify
   Sandia National Laboratories\[rs] Score processor using
   Event\-B. The processor is an (almost complete)
   implementation of a Java Virtual Machine in hardware. Thus,
   refinement\-based verification of the Score processor begins
   with a formal specification of Java bytecode. Traditionally,
   B has been directed at the formal development of software
   systems. The use of B in hardware verification could provide
   a means of developing combined software/hardware systems,
   i.e. codesign.