Return-Path:
Return-Path: <john.harrison-request@uk.ac.cam.cl>
Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP) to cl
          id <03493-0@swan.cl.cam.ac.uk>; Thu, 10 Oct 1991 18:20:06 +0100
Received: from hplb.hpl.hp.com by ted.cs.uidaho.edu (15.11/1.34) id AA00665;
          Thu, 10 Oct 91 08:54:50 pdt
Received: from acamille.hpl.hp.com by hplb.hpl.hp.com;
          Thu, 10 Oct 91 16:33:16 +0100
Received: by eeyore.hpl.hp.com (15.11/15.6+ISC) id AA17491;
          Thu, 10 Oct 91 16:40:14 bst
From: Albert Camilleri <ac@com.hp.hpl.hplb>
Message-Id: <9110101540.AA17491@eeyore.hpl.hp.com>
Subject: Temporary Vacancy at HP Labs, Bristol
To: info-hol@edu.uidaho.cs.ted (info-hol)
Date: Thu, 10 Oct 91 16:40:13 BST
Cc: fkh@uk.ac.ukc, sifakis@fr.imag.vercors,
    prinetto%itopoli.BITNET@edu.cuny.cunyvm,
    inverard%icnucevm.BITNET@edu.cuny.cunyvm, victoria@uk.ac.rhbnc.cs,
    ms@uk.ac.gla.cs, howard@uk.ac.man.cs
X-Mailer: Elm [version 2.0 beta]

The Software Engineering Department at Hewlett-Packard Laboratories,
Bristol, is looking for a researcher to temporarily join the
Hardware Verification Project, the current members of which are
Roger Fleming and myself.

The Harware Verification Project has been formally active since
October 1990. During this year it has been working actively with
designers in HP to formally analyse properties of a memory system
still in its design stages. The work, which involved proving liveness
and correct event ordering of this memory system, was successful
and the designers want to pursue further collaborations. Indeed we
are also seeking to establish new collaborations with other HP
divisions. For this reason we are seeking the expertise, advice
and skills of a third person who would partake in the research.
We have not yet decided on the future direction of our work and are
presently considering various research problems. From this point of
view, the timing for someone to join is excellent.

Anyone with a background in theorem proving and/or model checking
would be a likely candidate. Some knowledge of hardware and computer
architecture is desirable but not essential. We are especially interested
in developing a methodology which incorporates various verification
techniques, e.g. model checking and theorem proving. Applicants
would be expected to be somewhat flexible and willing to work in
problem areas not necessarily directly relating to their previous work.

The vacancy is typically one offered to post-graduate students
wishing to spend some time doing research in an industrial
laboratory environment, but of course, anybody interested can apply.
In fact, the post can be easily seen as a post-doc or sabbatical
opportunity. The salary varies according to experience and will be
discussed with prospective applicants.

Both the starting date and the duration of the post are negotiable,
but ideally, we are looking for someone prepared to start sometime
around January 1992, for a duration of 6-9 months.

Anyone interested and wanting further information should contact
either Roger Fleming (raf@hpl.hp.co.uk) or Albert Camilleri
(ac@hpl.hp.co.uk) (or both) as soon as possible. Alternatively
phone me on 0272 228196, or Roger Fleming on 0272 228712.

Albert Camilleri
10/10/91

