From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id p9OB6tHC005281 for ; Mon, 24 Oct 2011 13:06:55 +0200 X-IronPort-AV: E=Sophos;i="4.69,397,1315173600"; d="scan'208";a="125561244" Received: from walapai.inria.fr ([128.93.30.24]) by mail1-relais-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 24 Oct 2011 13:06:50 +0200 Received: from walapai.inria.fr (localhost [127.0.0.1]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id p9OB6omM005278 for ; Mon, 24 Oct 2011 13:06:50 +0200 Received: (from sympa@localhost) by walapai.inria.fr (8.13.6/8.12.10/Submit) id p9OB6oBj005277 for caml-list@inria.fr; Mon, 24 Oct 2011 13:06:50 +0200 Date: Mon, 24 Oct 2011 13:06:50 +0200 X-Authentication-Warning: walapai.inria.fr: sympa set sender to sympa@inria.fr using -f To: caml-list@inria.fr From: Cristiano Calcagno In-Reply-To: Message-ID: MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: 8bit Subject: [Caml-list] Research Engineer at Monoidics, London, UK Monoidics Ltd (www.monoidics.com), a high-tech SME specialising in automatic formal verification and producer of the INFER static analyzer is looking for a Research Engineer (3 years) to work on the EU Strep project CARP (Correct and Efficient Accelerator Programming), funded by the European Union. Other partners in the project are Imperial College, UK; Realeyes, Estonia; ARM, UK; RTWH Aachen, Germany; University of Twente, The Netherland; ENS, France and Rightware, Finland. Within the context of the CARP project, the research engineer will work on the development of tools and techniques for logic-based verification/static analysis for accelerator programming. Qualifications and Skills required: - PhD degree in Computer Science (or an equivalent qualification). - strong programming skills (in particular OCaml, but also C/C++/Java/system programming/embedded) - good background knowledge of static analysis, verification, concurrency, logic, compilers and formal methods. Starting date: December 1st, 2011, or as soon as possible thereafter. Location: London, UK Salary: Competitive For further information contact: Dr. Dino Distefano (dino.distefano@monoidics.com) =============================================================== About Monoidics: Monoidics is a high-tech SME specialising in automatic formal verification and analysis of software. Founded in the beginning of 2009 by a group of computer scientists from London and Cambridge, Monoidics designs automatic verification technology for safety critical industrial software. Monoidics' mission is to bring verification and program analysis research to the forefront of industrial practice. Based in London, Monoidics operates world-wide and has strong links with key industrial players in safety critical systems in Europe, USA, and Japan. =============================================================== About the CARP project: In recent years, massively parallel accelerator processors, primarily GPUs, have become widely available to end-users. Accelerators offer tremendous compute power at a low cost, and tasks such as media processing, simulation, medical imaging and eye-tracking can be accelerated to beat CPU performance by orders of magnitude. Performance is gained in energy efficiency and execution speed, allowing intensive media processing software to run in low-power consumer devices. Accelerators present a serious challenge for software developers. A system may contain one or more of the plethora of accelerators on the market, with many more products anticipated in the immediate future. Applications must exhibit portable correctness, operating correctly on any configuration of accelerators, and portable performance, exploiting processing power and energy efficiency offered by a wide range of devices. The overall aims of CARP are to design techniques and tools for correct and efficient accelerator programming: - Novel & attractive methods for constructing system-independent accelerator programs - Advanced code generation techniques to produce highly optimised system-specific code from system-independent programs - Scalable static techniques for analysing system-independent and system-specific accelerator programs, both qualitatively and quantitatively.