Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Mon, 14 Nov 1994 13:21:16 +0000
Received: by leopard.cs.byu.edu (1.38.193.4/16.2) id AA20978;
          Mon, 14 Nov 1994 06:15:48 -0700
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Received: from chirk.cam.sri.com by leopard.cs.byu.edu 
          with SMTP (1.38.193.4/16.2) id AA20973;
          Mon, 14 Nov 1994 06:14:35 -0700
Received: by chirk.cam.sri.com (4.1/SMI-4.1) id AA10123;
          Mon, 14 Nov 94 13:06:13 GMT
Date: Mon, 14 Nov 94 13:06:13 GMT
From: rwsh@cam.sri.com (Roger Hale)
Message-Id: <9411141306.AA10123@chirk.cam.sri.com>
To: hvg@cam.sri.com, info-hol@leopard.cs.byu.edu
Subject: [Ben.Moszkowski@newcastle.ac.uk: RA Post in Formal Methods and 
         Hardware]

From: Ben.Moszkowski@newcastle.ac.uk
Date: Mon, 14 Nov 1994 12:59:33 GMT
Subject: RA Post in Formal Methods and Hardware


			  RESEARCH ASSISTANT
			 Computer Engineering
				       
	      Dept Electrical & Electronic Engineering,
	       University of Newcastle-upon-Tyne, U.K.


Applications are invited for the post of Research Assistant on a
three-year EPSRC-funded project in the area of applied formal systems
design.  Applicants should have a good degree in Electronic
Engineering with a strong computing content, and it would be of
advantage to have the following background:

- Interest and experience in formal design methods, possibly including
  modal and temporal logics;

- Experience in digital hardware design.

Existing work at Newcastle includes projects in the area of formal
design and verification techniques, and work in advanced computer
design.  The present applicant is sought for a new project which
bridges both these areas, aiming to accomplish a provably-correct
design for an existing CPU.

Previous work at Newcastle in formal design has involved research on
the use of Interval Temporal Logic, a formalism for reasoning about
multi-level timing dependent hardware and software systems.  Ongoing
work includes the development of compositional properties to
facilitate modular verification of the correctness of concurrent
systems.  Previous work in processor design has included the
development of an advanced dataflow processor in ECL technology, as an
exploratory vehicle for dataflow programming techniques and
algorithms.  The present project will involve the application of newly
developed formal logic techniques to the redesign of the processor,
and will be carried out in collaboration with Dr B.C. Moszkowski and
Dr J.N. Coleman.

The post is of approximately 3 years' duration, and carries a salary
in the region of 15,000 pounds p.a.  Potential applicants are welcome
to contact Dr Coleman on 091 222 7860 or Dr Moszkowski by email
address Ben.Moszkowski@ncl.ac.uk for an informal discussion prior to
submitting an application, which should consist of a full C.V.
together with the names and addresses of three referees.

Applications will continue to be accepted until the post is filled,
but an initial evaluation will be made on 12th December, 1994.  They
should be sent to Dr J.N. Coleman, Department of Electrical and
Electronic Engineering, The University, Newcastle-upon-Tyne, NE1 7RU.




