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; Mon, 21 Aug 1995 17:16:24 +0100 Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA278119890; Mon, 21 Aug 1995 09:44:50 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: list Received: from mail.hud.ac.uk by leopard.cs.byu.edu with SMTP (1.37.109.15/16.2) id AA278009836; Mon, 21 Aug 1995 09:43:56 -0600 Received: from zeus.hud.ac.uk by mail.hud.ac.uk with SMTP (PP) id <14564-0@mail.hud.ac.uk>; Mon, 21 Aug 1995 16:40:13 +0100 Original-Received: from hera.csm by zeus.hud.ac.uk (4.1/SMI-4.1) Pp-Warning: Illegal Received field on preceding line Received: from efe.csm by hera.csm (4.1/SMI-4.1) id AA11157; Mon, 21 Aug 95 16:39:52 BST Date: Mon, 21 Aug 95 16:39:52 BST From: scomaw@zeus.hud.ac.uk (Ann Wrightson) Message-Id: <9508211539.AA11157@hera.csm> To: isabelle-users@cl.cam.ac.uk, info-hol@leopard.cs.byu.edu, bra-types@cs.chalmers.se Subject: Research studentship Cc: scomaw@zeus.hud.ac.uk Research studentship available NOW in the School of Computing and Mathematics, University of Huddersfield, UK PLEASE RESPOND QUICKLY - IF THERE IS NO-ONE IN PLACE BY 1 OCT THIS OPPORTUNITY VANISHES!!! Subject area: Requirements/Applied Logic Title: Situation Logic for Requirement Information Flow Staff: Ann Wrightson, Prof Lee McCluskey Recent work here has yielded a framework for describing exactly the semantics of information flowing into a system development, providing a clear and explicit semantic link between informal requirements expressed in natural language, and formal description of system elements. The research student will develop a key part of this framework into a fully specified logic suitable for automated reasoning, as might be used in automated support for requirements engineering. This will be built as an object-logic for the ``Isabelle'' generic theorem-prover. The research student will need a good first degree or equivalent in computer science or a related discipline, and in particular a sound knowledge of first-order logic, and general knowledge of computer systems development. He or she will ideally also be familiar with the ML language used in ``Isabelle'', and have a specific interest in applied logic and/or requirements engineering. This studentship is *not* restricted to UK/EEC nationals, but the timescale is of the essence, which I guess restricts things in practice. Further information available from Ann Wrightson, a.wrightson@hud.ac.uk -------------------------------------------------------------- Ann M Wrightson Senior Lecturer School of Computing and Mathematics University of Huddersfield Queensgate Tel: (01484) 472758 Huddersfield Fax: (01484) 421106 HD1 3DH UK --------------------------------------------------------------