From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by yquem.inria.fr (Postfix) with ESMTP id 9D48ABBBB for ; Fri, 10 Feb 2006 16:22:55 +0100 (CET) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id k1AFMtGk022349 for ; Fri, 10 Feb 2006 16:22:55 +0100 Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id QAA28944 for ; Fri, 10 Feb 2006 16:22:54 +0100 (MET) Received: from mail-eur1.microsoft.com (mail-eur1.microsoft.com [213.199.128.139]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id k1AFMsOm001822 for ; Fri, 10 Feb 2006 16:22:54 +0100 Received: from EUR-MSG-21.europe.corp.microsoft.com ([65.53.210.18]) by mail-eur1.microsoft.com with Microsoft SMTPSVC(6.0.3790.1830); Fri, 10 Feb 2006 15:22:54 +0000 X-MimeOLE: Produced By Microsoft Exchange V6.5 Content-class: urn:content-classes:message MIME-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: quoted-printable Subject: Position available for O'Caml programmer in Microsoft's TERMINATOR project Date: Fri, 10 Feb 2006 15:22:52 -0000 Message-ID: <5CB6E17938E03B4E9DC2187DC2B5FA7502EFE539@EUR-MSG-21.europe.corp.microsoft.com> Thread-Topic: Position available for O'Caml programmer in Microsoft's TERMINATOR project Thread-Index: AcYuVdnik6LLE4ytSK2dmoivfpyp6w== From: "Byron Cook" To: X-OriginalArrivalTime: 10 Feb 2006 15:22:54.0014 (UTC) FILETIME=[DCEB3DE0:01C62E55] X-Miltered: at nez-perce with ID 43ECAFCF.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at concorde with ID 43ECAFCE.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; o'caml:01 arbitrarily:01 recursive:01 pointers:01 abstraction:01 infers:01 invariants:01 ml-like:01 o'caml:01 compilers:01 prolog:01 functions:01 functions:01 termination:01 termination:01 X-Spam-Checker-Version: SpamAssassin 3.0.3 (2005-04-27) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.0.3 Research Software Development Engineer: TERMINATOR project Project website: http://www.research.microsoft.com/terminator Site location: Microsoft Research in Cambridge, UK Contract length: 6 months to start, with negotiation to extend Who to contact: Byron Cook (bycook@microsoft.com) TERMINATOR is a program termination prover that supports C programs with arbitrarily nested loops or recursive functions, and imperative features such as references, functions with side-effects, and function pointers. TERMINATOR uses a newly discovered method of counterexample-guided abstraction refinement for program termination proofs. The termination argument is constructed incrementally, based on failed proof attempts. TERMINATOR also infers and proves required program invariants on demand. It has been successfully used on Windows device drivers of up to 35,000 lines of code. The TERMINATOR team is looking for someone with functional programming and formal verification experience to develop and maintain the TERMINATOR code-base. Candidates should have the following qualifications: 1) MS. or Ph.D. in Computer Science 2) Experience with ML or an ML-like programming language (TERMINATOR is written primarily in O'Caml, with some C++ and Prolog) 3) Knowledge of algorithms and techniques from automatic formal verification and compilers 4) Good communication and inter-personal skills 5) Leadership and cross-team collaboration skills 6) 2 years of industrial experience (preferred) This position will include the following activities: Fixing bugs in the TERMINATOR code base; providing new features in TERMINATOR; responding to customer feature requests; improving the performance of TERMINATOR, and improving the reliability of TERMINATOR. This is an important position. TERMINATOR is the first known automatic termination prover to support real programs, and solves a problem that is important to reactive systems (i.e. proving that they actually will be able to react). It has the potential to make a huge contribution to how future developers write programs and the quality of the software that we use. Interested? Send a CV to Byron Cook (bycook@microsoft.com)