From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=1.0 required=5.0 tests=AWL,MISSING_HEADERS, SORTED_RECIPS autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by yquem.inria.fr (Postfix) with ESMTP id 5550EBB84 for ; Thu, 22 May 2008 10:44:42 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AvIBAOvPNEjAXQIniGdsb2JhbACSNAEBAQ8gC5xq X-IronPort-AV: E=Sophos;i="4.27,524,1204498800"; d="scan'208";a="10986020" Received: from concorde.inria.fr ([192.93.2.39]) by mail2-smtp-roc.national.inria.fr with ESMTP; 22 May 2008 10:44:41 +0200 Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id m4M8ie8d016810 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Thu, 22 May 2008 10:44:41 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AsUAAPLONEiG4iA4nWdsb2JhbACSNAEBAQEBCA0HHJxv X-IronPort-AV: E=Sophos;i="4.27,524,1204498800"; d="scan'208";a="26496035" Received: from relay.cs.tcd.ie (HELO cs.tcd.ie) ([134.226.32.56]) by mail4-smtp-sop.national.inria.fr with ESMTP; 22 May 2008 10:44:40 +0200 Received: from localhost (localhost [127.0.0.1]) by relay.cs.tcd.ie (Postfix) with ESMTP id 4B37453F9D; Thu, 22 May 2008 09:44:39 +0100 (IST) X-Virus-Scanned: amavisd-new at cs.tcd.ie Received: from cs.tcd.ie ([127.0.0.1]) by localhost (smtp.cs.tcd.ie [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id y9gAQU2Ki8lJ; Thu, 22 May 2008 09:44:38 +0100 (IST) Received: from [134.226.35.226] (saoithin.cs.tcd.ie [134.226.35.226]) by smtp.cs.tcd.ie (Postfix) with ESMTP id 03AE053EF5; Thu, 22 May 2008 09:44:35 +0100 (IST) Message-ID: <4835326E.4090806@cs.tcd.ie> Date: Thu, 22 May 2008 09:44:30 +0100 From: Andrew Butterfield User-Agent: Thunderbird 2.0.0.14 (Windows/20080421) MIME-Version: 1.0 Cc: agents@cs.umbc.edu, appsem@lists.tcs.ifi.lmu.de, caml-list@inria.fr, comlab@comlab.ox.ac.uk, coq-club@pauillac.inria.fr, lfcs-interest@dcs.ed.ac.uk, logic-list@Helsinki.FI, nvti-list@cwi.nl, petrinet@informatik.uni-hamburg.de, procos@jiscmail.ac.uk, prog-lang@diku.dk, seworld@cs.colorado.edu, theory-logic@cs.cmu.edu Subject: Funded PhD position: formalising hardware/software interface References: <000c01c8bbdd$03b095d0$b50112ac@nb5279> In-Reply-To: <000c01c8bbdd$03b095d0$b50112ac@nb5279> Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit X-Miltered: at concorde with ID 48353278.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; supervisor:01 model:01 unifying:01 o'reilly:01 tcd:98 tcd:98 dublin:98 vdm:98 dublin:98 calculus:01 variant:02 theorem:02 motivation:02 implemented:02 face:97 3-year funded Ph.D. position Formalising the Interface between Software and Hardware (FISH) https://www.cs.tcd.ie/Andrew.Butterfield/FISH/ Start Date: September/October 2008 Team: Foundations and Methods Group, Software Systems Laboratory, Trinity College Dublin Supervisor: Andrew Butterfield Andrew.Butterfield@cs.tcd.ie Summary The aim of this project is to investigate the modelling of the interface between hardware and software, with particular emphasis on Flash Memory devices. The motivation for this work is to be able to contribute to a formally verified model of a POSIX-aware file-store implemented with flash memory, and so suitable for mission-critical data-collection applications such as space probes. This is part of a pilot project currently under way in the Grand Challenge on Dependable Systems Evolution. The research will use the techniques of the Unifying Theories of Programming (UTP), and recent work on the language "Circus", and a variant called "slotted-Circus", to explore the theory and practise of reasoning about the correctness of software at the hardware interface level, incorporating techniques for reasoning about the correctness in the face of certain classes of failure whose occurrence is probabilistic and non-determinisitic. We seek a student with an interest in modelling and verification, with experience of at least one formal method (Z, VDM, B, CSP, pi-Calculus) and skills with discrete mathematics, predicate calculus and theorem proving. The candidate should have a good background in computer science, with a good Bachelors or MSc degree in Computer Science, Mathematics or a similar area. The funding covers fees, plus a stipend of 17,000+ euros. Applications: Send applications, by email to mailto:Andrew.Butterfield@cs.tcd.ie?Subject=FISH, containing: 1. Detailed CV 2. Contact details for at least two referees 3. A clear statement as to why you would be suited for this research project. See the project website for further details https://www.cs.tcd.ie/Andrew.Butterfield/FISH/ -- -------------------------------------------------------------------- Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204 Foundations and Methods Research Group Director. School of Computer Science and Statistics, Room F.13, O'Reilly Institute, Trinity College, University of Dublin http://www.cs.tcd.ie/Andrew.Butterfield/ --------------------------------------------------------------------