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.8 required=5.0 tests=AWL,DNS_FROM_RFC_ABUSE, SPF_SOFTFAIL 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 DAB71BC6B for ; Sat, 13 Oct 2007 17:35:55 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAEaCEEfAXQInh2dsb2JhbACOSAEBAQgKKYEn X-IronPort-AV: E=Sophos;i="4.21,270,1188770400"; d="scan'208";a="2967792" Received: from concorde.inria.fr ([192.93.2.39]) by mail2-smtp-roc.national.inria.fr with ESMTP; 13 Oct 2007 17:35:55 +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 l9DFZrXR002943 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Sat, 13 Oct 2007 17:35:55 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAPqCEEfVx4q/n2dsb2JhbACOSAEBAQEHBAYJIIEn X-IronPort-AV: E=Sophos;i="4.21,270,1188770400"; d="scan'208";a="17947460" Received: from smtp-dub.microsoft.com ([213.199.138.191]) by mail4-smtp-sop.national.inria.fr with ESMTP; 13 Oct 2007 17:35:44 +0200 Received: from dub-exhub-c302.europe.corp.microsoft.com (65.53.213.92) by DUB-EXGWY-E801.partners.extranet.microsoft.com (10.251.129.1) with Microsoft SMTP Server (TLS) id 8.1.177.2; Sat, 13 Oct 2007 16:35:43 +0100 Received: from EA-EXMSG-C315.europe.corp.microsoft.com ([65.53.221.36]) by dub-exhub-c302.europe.corp.microsoft.com ([65.53.213.92]) with mapi; Sat, 13 Oct 2007 16:35:42 +0100 From: Don Syme To: "caml-list@inria.fr" Date: Sat, 13 Oct 2007 16:35:39 +0100 Subject: Microsoft Research Cambridge Lab Vacancy - Research Software Development Engineer Thread-Topic: Microsoft Research Cambridge Lab Vacancy - Research Software Development Engineer Thread-Index: AcYXjn0A2ALAwyPwTuS+ifYn3EcZS1al//HwAC8TjFAAB9NPMAAAUMOQBhAOQQAAVzUdcALGOdkAAAEZheAdSqU68AAAYF/gAAEWSMAAMCAS8A== Message-ID: <7E24A64DB2F6F34E8C6002C4EB2344971B6A7FF1CC@EA-EXMSG-C315.europe.corp.microsoft.com> Accept-Language: en-US Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: acceptlanguage: en-US Content-Type: text/plain; charset="iso-8859-1" Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 X-Miltered: at concorde with ID 4710E5D9.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; syme:01 syme:01 compiler:01 ml-like:01 ocaml:01 angles:98 2007.:98 termination:01 algorithms:03 verifier:03 verifier:03 internals:03 cambridge:03 cambridge:03 static:03 Job Title: Research Software Development Engineer (RSDE) Group: Terminator and SLAyer team / Programming Principles and Tools Location: Microsoft Research, Cambridge (UK) Start date: Flexible Description: SLAyer is a software analysis tool that automatically proves properties abo= ut the data-structures constructed/modified by concurrent systems-level cod= e. Terminator is an additional componenet designed to prove termination an= d liveness properties. The joint SLAyer/Terminator team is looking for a d= eveloper interested in building the first production version of these tools= . This position is in Microsoft's Research division. It will involve a clos= e partnership with Windows Static Driver Verifier team in Redmond, WA. This position will include: * Developing the internal components within Terminator and SLAyer * Integrating Terminator and SLAyer with the Static Driver Verifier product * Developing additional infrastructure for future program verification tool= s For more information about Terminator and SLAyer see: * http://research.microsoft.com/TERMINATOR * http://research.microsoft.com/SLAyer Candidates should have the following technical qualifications: * MS. or Ph.D. in Computer Science * 2+ years development experience highly desirable (e.g. experience shippin= g software) * Knowledge of algorithms and techniques of program analysis is necessary, = at least, from one of the two angles: formal verification or compiler desig= n. It is expected to be based on college education or 2+ years of industria= l experience. * Experience with ML-like programming language (F#, OCaml) is highly desira= ble * Knowledge of and experience with OS internals or driver development is a = plus * Good communication and inter-personal skills * Leadership abilities and cross-team collaboration skills To apply or request further details, please contact our Human Resources Dep= artment by email: cambhr@microsoft.com Closing date for applications is Friday, 30 November 2007. Microsoft Research is an equal opportunities employer