Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Tue, 18 Jul 1995 20:57:01 +0100 Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA066603485; Tue, 18 Jul 1995 10:04:45 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: list Received: from swan.cl.cam.ac.uk by leopard.cs.byu.edu with ESMTP (1.37.109.15/16.2) id AA066413415; Tue, 18 Jul 1995 10:03:35 -0600 Received: from dunlin.cl.cam.ac.uk (user lcp (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Tue, 18 Jul 1995 17:03:38 +0100 X-Mailer: exmh version 1.6.1 5/23/95 To: isabelle-users@cl.cam.ac.uk, bra-types@cs.chalmers.se, info-hol@leopard.cs.byu.edu Subject: research post available X-Uri: X-Face: "OrDM]eXxWpb;,!g'n)u!-ss/8qvWB4*r>rA5~IAaMPwt$YO^oBckRP3N&D0.K"wKN7B> E&BJ5P-gy=o">rX=;.8M:sNp55m9?O%dK#v4{5e#8=-q9FUHURBbRfE:g\DybYQW4~MkQ 13swsz`i*9}*8fy}.au9jo. Date: Tue, 18 Jul 1995 17:03:30 +0100 From: Lawrence C Paulson Message-Id: <"swan.cl.cam.:233960:950718160346"@cl.cam.ac.uk> Dear colleagues, Please forward this job advertisement to any suitable candidates. It is also available on the World Wide Web at URL http://www.cl.cam.ac.uk/users/lcp/Temporal/announce.html Thanks! Larry Paulson University of Cambridge Computer Laboratory RESEARCH ASSISTANT: MECHANISING TEMPORAL REASONING The EPSRC project "Mechanising Temporal Reasoning" will run for three years starting in October 1995. The project involves building an environment for temporal reasoning on top of the theorem prover Isabelle. For more details please see the URL http://www.cl.cam.ac.uk/users/lcp/Temporal/temp.html The project includes improving Isabelle's support for Lamport's TLA, providing support for UNITY, and linking Isabelle to the model checker SMV. It could include linking Isabelle to other tools such as decision procedures, and investigating how such linking can be performed safely. The research assistant will be responsible for most of these tasks, which the work plan describes in detail. The ideal candidate will have a PhD in Computer Science, experience with Isabelle, HOL, PVS or a similar system, and knowledge of temporal logic. The salary will be up to 15566 pounds (UK) per annum depending on qualifications and experience. If a successful applicant has exceptional experience, we may be able to negotiate an increase from the EPSRC. Appointment will be for 12 months in the first instance, and will be extended by a further 24 months should the arrangement prove mutually satisfactory. Applications, including curriculum vitae and the names of two referees, should be sent by 14th August 1995 to Dr L. C. Paulson at the address below. The University follows an equal opportunities policy. Lawrence C Paulson, University Lecturer Computer Laboratory, University of Cambridge, Pembroke Street, Cambridge CB2 3QG, England Tel: +44(0)1223 334623 Fax: +44(0)1223 334678