From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id 3E9837EE51 for ; Thu, 11 Apr 2013 22:23:33 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of tom.j.ridge@googlemail.com) identity=pra; client-ip=209.85.192.179; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="tom.j.ridge@googlemail.com"; x-sender="tom.j.ridge@googlemail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of tom.j.ridge@googlemail.com designates 209.85.192.179 as permitted sender) identity=mailfrom; client-ip=209.85.192.179; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="tom.j.ridge@googlemail.com"; x-sender="tom.j.ridge@googlemail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-pd0-f179.google.com) identity=helo; client-ip=209.85.192.179; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="tom.j.ridge@googlemail.com"; x-sender="postmaster@mail-pd0-f179.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AloCAHgaZ1HRVcCzlWdsb2JhbABQDoMuwkgIFg4BAQEBBw0JCRIqgmYBATgQFV0SAQUBIgGIEwEDDwyedIpvhDsBBYRxChknDYlXBo1UhQqTOYNMgSGODBYpgVmCFkA7gTAHFwY X-IPAS-Result: AloCAHgaZ1HRVcCzlWdsb2JhbABQDoMuwkgIFg4BAQEBBw0JCRIqgmYBATgQFV0SAQUBIgGIEwEDDwyedIpvhDsBBYRxChknDYlXBo1UhQqTOYNMgSGODBYpgVmCFkA7gTAHFwY X-IronPort-AV: E=Sophos;i="4.87,458,1363129200"; d="scan'208";a="10660549" Received: from mail-pd0-f179.google.com ([209.85.192.179]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 11 Apr 2013 22:23:32 +0200 Received: by mail-pd0-f179.google.com with SMTP id x11so1027454pdj.24 for ; Thu, 11 Apr 2013 13:23:30 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlemail.com; s=20120113; h=x-received:mime-version:sender:from:date:x-google-sender-auth :message-id:subject:to:content-type; bh=2Z0jfXO9OKorXC+HM9hJTqc5fcukt8I+j+kWeMFfBjc=; b=ltD3d4WDcmbR5H7KWXOP7u8EgzqZ9G3Sn7c/w4Y8W4Bb5An/vk7mDJM4DdPggjArVs XnFJ/sPkT1tNivFhw+Y9BSUn1cgXbjxX0YAeN3p4ZsVXop4sDoMwbMAfalpKf5Le0jCX CDG/dYjXzo8X3s59gRRX2I1NxelIfbIf/XcEa88+pVTzGhoZYoXXVkSbSz1ZR0LKGpN5 1t2JNjlltatQte7KZ2Fbbmn/Qhn5+F8eCx8MxJE/qD9udC5AMxgnj5SBFoxLi1SlSKA/ LdjRdG0Xmcw2XlXwRvgGfyuHk3ZICgj+jt+lNk1ZVZSc2z2qA30OBrP+5Ue94dUgyWJQ DWfA== X-Received: by 10.68.229.163 with SMTP id sr3mr10904304pbc.54.1365711810259; Thu, 11 Apr 2013 13:23:30 -0700 (PDT) MIME-Version: 1.0 Sender: tom.j.ridge@googlemail.com Received: by 10.70.42.3 with HTTP; Thu, 11 Apr 2013 13:23:10 -0700 (PDT) From: Tom Ridge Date: Thu, 11 Apr 2013 21:23:10 +0100 X-Google-Sender-Auth: cuCYy8bgEkOZklY20xVz_xXyQYE Message-ID: To: acl2@utlists.utexas.edu, agda@lists.chalmers.se, caml-list , cl-mirage@lists.cam.ac.uk Content-Type: text/plain; charset=ISO-8859-1 X-Validation-by: tom.j.ridge@googlemail.com Subject: [Caml-list] Microsoft-funded PhD opportunity (software/ system verification) Dear Colleagues, I would be very grateful if you could bring the following advert to the attention of potential applicants. Also, if anyone if interested in the project, please do get in touch! Thanks Tom -- Microsoft Research PhD studentship: Future Filesystems ====================================================== Project: Future filesystems: mechanized specification, validation, implementation and verification of filesystems Supervisors: Tom Ridge (with Andrew Kennedy at Microsoft Research) Application deadline: 2013-06-02 (June 2nd) PhD expected start date: 2013-10-01 We seek strong candidates for a Microsoft PhD studentship on "verified filesystems". The PhD scholarship is fully funded for three years. The project will be supervised by Tom Ridge at the Department of Computer Science, University of Leicester, in collaboration with Andrew Kennedy at Microsoft Research Cambridge. Project description ------------------- Filesystems are extremely important. Users depend on filesystems to store their files whenever they hit "save". Businesses rely on databases to store their data safely, and these databases in turn rely on the filesystem. Modern filesystems are designed to satisfy many complicated requirements. As a result, implementations are beset with problems. The implementation code is extremely complex, and almost inevitably contains bugs. These bugs can and do lead to data corruption and loss. Development time is very lengthy. Testing is also very lengthy and costly, and does not guarantee to eliminate all bugs. It is often unclear to application developers what guarantees a filesystem provides, so that it becomes extremely difficult to write correct applications for a given filesystem, let alone applications that are portable across different filesystems. In this project, we aim to tackle these problems by applying formal methods techniques. We will specify the behaviour of existing filesystems using higher-order logic (supported by the HOL4 theorem prover). Further, we will implement a filesystem, and verify functional correctness of the implementation with respect to the specification. We are particularly interested in the behaviour of filesystems when the host crashes. The project involves theoretical aspects (for example, we are interested in understanding the dependencies that arise when different filesystem operations execute; the project will also involve extensive proofs, both informal and mechanized) but is focused on applications of theory to real-world systems. Background of applicant ----------------------- Ideally the applicant should be a good programmer (with knowledge of one of the main functional programming languages such as OCaml, Haskell, SML etc), with background in semantics (particularly operational semantics), theorem proving, and verification. The applicant must have a strong interest in producing reliable systems. Applicants should hold at least a good second-class honours degree or equivalent in computer science (or a closely related discipline) and have a good command of English. A masters degree may be an advantage, but is not necessary. Funding ------- The Microsoft scholarship consists of an annual bursary for 3 years. This studentship is fully funded (fees and stipend) for UK and EU students. The stipend is up to 17,000 UK pounds. We welcome overseas applicants, and would provide the equivalent of home/EU fees and maintenance for a successful overseas candidate; the difference between home/ EU fees and international fees (approx. 11,000 UK pounds per annum) would need to be funded by the overseas applicant. Environment ----------- The Department of Computer Science offers a highly collegiate and stimulating environment for research career development. The prospective student will work within an ambitious research team that is internationally recognised and will be expected to contribute to the strong profile of the department through participation in the development and publication of international-quality research results. Application process ------------------- We encourage potential applicants who wish to express their interest in the project to email Tom Ridge `tr61 (at) le.ac.uk` well before the deadline. The application process is via the University of Leicester. For further details on the application process, see Further questions ----------------- Please contact Tom Ridge `tr61 (at) le.ac.uk` if you have any further questions.