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 mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 0D3347F0D9 for ; Wed, 26 Aug 2015 17:21:27 +0200 (CEST) IronPort-PHdr: 9a23:9mVhzRA7C6FcY15c8VuEUyQJP3N1i/DPJgcQr6AfoPdwSP/6ocbcNUDSrc9gkEXOFd2CrakU0KyI6uuwByQp2tWojjMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpQAbFhi3DwdpPOO9QteU1JTskb7rsM2NKyxzxxODIppKZC2sqgvQssREyaBDEY0WjiXzn31TZu5NznlpL1/A1zz158O34YIxu38I46Fp34d6XK77Z6U1S6BDRHRjajhtpZ6jiR6WcQuCrlAVV2FetxNJBwnD41neX4zt+n/xv+95nS2bJtHeTLYuWD3k4b09GyXlkCMWCzls+mbNi9dYnatYpximuAd8wsjTeo7GGuB5e/b3eskbXiJwV8VWXSteGYC9J98FCPAAJs5Jpor6rVwRthi/Qw62C7W8mXdzmnbq0PhigKwaGgbc0VllRopWvQ== Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=boris@yakobowski.org; spf=Pass smtp.mailfrom=boris@yakobowski.org; spf=None smtp.helo=postmaster@19.mo3.mail-out.ovh.net Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of boris@yakobowski.org) identity=pra; client-ip=178.32.98.231; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="boris@yakobowski.org"; x-sender="boris@yakobowski.org"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of boris@yakobowski.org designates 178.32.98.231 as permitted sender) identity=mailfrom; client-ip=178.32.98.231; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="boris@yakobowski.org"; x-sender="boris@yakobowski.org"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@19.mo3.mail-out.ovh.net) identity=helo; client-ip=178.32.98.231; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="boris@yakobowski.org"; x-sender="postmaster@19.mo3.mail-out.ovh.net"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0BfAQAs2d1VnOdiILJDGoNvaQEFgx28S4I/g0aBJwc8EAEBAQEBAQEBEAEBAQEBBg0JCSEugh2CHxFIBi43AiQSAQUBIhMUDogMBAEIPKNWggWBLz4xi0CGWI5UiliFKhEBgQmCOIFDBZU5cIwCT3uEMoMejVmCHxIjgRcXgVkMgitvgQcHFweBIQEBAQ X-IPAS-Result: A0BfAQAs2d1VnOdiILJDGoNvaQEFgx28S4I/g0aBJwc8EAEBAQEBAQEBEAEBAQEBBg0JCSEugh2CHxFIBi43AiQSAQUBIhMUDogMBAEIPKNWggWBLz4xi0CGWI5UiliFKhEBgQmCOIFDBZU5cIwCT3uEMoMejVmCHxIjgRcXgVkMgitvgQcHFweBIQEBAQ X-IronPort-AV: E=Sophos;i="5.17,416,1437429600"; d="scan'208";a="174940263" Received: from 19.mo3.mail-out.ovh.net ([178.32.98.231]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/ADH-AES256-GCM-SHA384; 26 Aug 2015 17:21:26 +0200 Received: from mail614.ha.ovh.net (gw6.ovh.net [213.251.189.206]) by mo3.mail-out.ovh.net (Postfix) with SMTP id 5E4C0FFC876 for ; Wed, 26 Aug 2015 17:21:25 +0200 (CEST) Received: from localhost (HELO queueout) (127.0.0.1) by localhost with SMTP; 26 Aug 2015 17:21:24 +0200 Received: from mail-lb0-f176.google.com (boris@yakobowski.org@209.85.217.176) by ns0.ovh.net with SMTP; 26 Aug 2015 17:21:22 +0200 Received: by lbbpu9 with SMTP id pu9so122125775lbb.3 for ; Wed, 26 Aug 2015 08:21:21 -0700 (PDT) X-Received: by 10.112.154.106 with SMTP id vn10mr31229752lbb.38.1440602481278; Wed, 26 Aug 2015 08:21:21 -0700 (PDT) MIME-Version: 1.0 Reply-To: boris@yakobowski.org Received: by 10.112.2.132 with HTTP; Wed, 26 Aug 2015 08:21:01 -0700 (PDT) From: Boris Yakobowski Date: Wed, 26 Aug 2015 17:21:01 +0200 Message-ID: To: The Caml Mailing List Content-Type: multipart/alternative; boundary=089e0122af2a28c784051e38673d X-Ovh-Tracer-Id: 15668586055102543904 X-Ovh-Remote: 209.85.217.176 (mail-lb0-f176.google.com) X-Ovh-Local: 213.186.33.20 (ns0.ovh.net) X-OVH-SPAMSTATE: OK X-OVH-SPAMSCORE: -100 X-OVH-SPAMCAUSE: gggruggvucftvghtrhhoucdtuddrfeekfedrieduucetufdoteggucfrrhhofhhilhgvmecuqfggjfenuceurghilhhouhhtmecufedttdenucesvcftvggtihhpihgvnhhtshculddquddttddm X-VR-SPAMSTATE: OK X-VR-SPAMSCORE: -100 X-VR-SPAMCAUSE: gggruggvucftvghtrhhoucdtuddrfeekfedrieduucetufdoteggucfrrhhofhhilhgvmecuqfggjfenuceurghilhhouhhtmecufedttdenucesvcftvggtihhpihgvnhhtshculddquddttddm X-Validation-by: boris@yakobowski.org Subject: [Caml-list] Open engineer & scientist positions at CEA LIST - LSL --089e0122af2a28c784051e38673d Content-Type: text/plain; charset=UTF-8 Hello, The LSL laboratory at CEA LIST [#] has open permanent positions. If you are interested, please consider applying. More details are available below. ==== Next generation tools for formal verification. ==== The LSL Software Security Laboratory helps developers and validation experts ship high-confidence software and systems. With everyday objects getting more and more complex, we have built a reputation for efficiently applying formal reasoning techniques to establish their trustworthiness. As part of the CEA LIST Institute, at the heart of Campus Paris Saclay, teams at LSL are researching the best possible means to conduct formal verification. We design tools such as Frama-C, GATeL, and UNISIM, that ensure production-level systems can comply with the highest safety and security standards. And in doing so, we get to interact with the most creative people in academia and the industry. Our organizational structure is simple: those who pioneer new concepts are the ones who get to lead their implementation. We are a fast-growing thirty-person team, and your work will have a direct and visible impact on the state of formal verification. == You == You dream of devising the next breakthrough in verification and to see it through low-level implementation details. You read research papers with a passion, but you are well aware that a toy prototype is quite different from a hardened tool. You understand that what stands between both is a series of challenging implementation problems. And that's great, because it means getting your hands dirty and coming up with ground-breaking code. You enjoy being a constructive member of a team of talented and dedicated people; you are extremely reliable and the nightly builds will prove it every time. Last week's bleeding-edge release of obscure packages is not really your thing. You want the source code, you want scalability, and you want results. If this sounds like you, we have a job for you. == Role == We need you to help us develop our formal tools and platforms, both by improving current verifiers and by designing new approaches. You will contribute to growing the community of users, handling feedback and helping real people solve real problems. You will take an active role in research activities and industrial partnerships, alongside other members of the laboratory. This can include writing proposals, managing projects, publishing papers, and attending scientific and technical events worldwide. == Requirements == - Background in formal methods and programming languages. - Hands-on experience with significant OCaml developments - other languages are fine too, but you'll need to convince us you can adapt in a snap. - Self-organized, with an ability to prioritize effectively. - Team-minded - you know when to let someone else take the lead. == Pluses == Various areas of our overall activity can also benefit from specific skillsets. - Break new ground with us: * Hands-on expertise in the fields of software security or hybrid systems. * Flawless understanding of `C++` and object-oriented semantics. - Precision-drive our infrastructure: * Technical administration of Linux environments and development tools. * Robust grasp of IT service management processes. - Help us spread the word: * Strong proficiency in foreign languages. * A knack for writing and editing longform content. == Applying == If you're interested in joining LSL, send us an email to share what inspires you, and why you think you are a good match for the team. Send it with a resume at florent.kirchner@cea.fr. [#] http://www-list.cea.fr/index.php/en/technological-research/research-programmes/embedded-systems/validation-and-verification -- Boris Yakobowski CEA LIST --089e0122af2a28c784051e38673d Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
Hello,

The LSL laboratory at CEA LIST [#= ] has open permanent positions.=C2=A0 If you are interested, please conside= r applying. More details are available below.


=3D=3D=3D=3D Next generation tools for formal verification. =3D=3D=3D=3D The LSL Software Security Laboratory helps developers and validation expert= s ship high-confidence software and systems. With everyday objects getting = more and more complex, we have built a reputation for efficiently applying = formal reasoning techniques to establish their trustworthiness. As part of the CEA LIST Institute, at the heart of Campus Paris Saclay, tea= ms at LSL are researching the best possible means to conduct formal verific= ation. We design tools such as Frama-C, GATeL, and UNISIM, that ensure production-= level systems can comply with the highest safety and security standards. An= d in doing so, we get to interact with the most creative people in academia= and the industry. Our organizational structure is simple: those who pioneer new concepts are = the ones who get to lead their implementation. We are a fast-growing thirty= -person team, and your work will have a direct and visible impact on the st= ate of formal verification. =3D=3D You =3D=3D You dream of devising the next breakthrough in verification and to see it t= hrough low-level implementation details. You read research papers with a pa= ssion, but you are well aware that a toy prototype is quite different from = a hardened tool. You understand that what stands between both is a series o= f challenging implementation problems. And that's great, because it mea= ns getting your hands dirty and coming up with ground-breaking code. You enjoy being a constructive member of a team of talented and dedicated p= eople; you are extremely reliable and the nightly builds will prove it ever= y time. Last week's bleeding-edge release of obscure packages is not re= ally your thing. You want the source code, you want scalability, and you wa= nt results. If this sounds like you, we have a job for you.
=3D=3D Role =3D=3D We need you to help us develop our formal tools and platforms, both by impr= oving current verifiers and by designing new approaches. You will contribut= e to growing the community of users, handling feedback and helping real peo= ple solve real problems. You will take an active role in research activities and industrial partners= hips, alongside other members of the laboratory. This can include writing p= roposals, managing projects, publishing papers, and attending scientific an= d technical events worldwide.
=3D=3D Requirements =3D=3D - Background in formal methods and programming languages. - Hands-on experience with significant OCaml developments - other languages= are fine too, but you'll need to convince us you can adapt in a snap. - Self-organized, with an ability to prioritize effectively. - Team-minded - you know when to let someone else take the lead.
=3D=3D Pluses =3D=3D Various areas of our overall activity can also benefit from specific skills= ets. - Break new ground with us: * Hands-on expertise in the fields of software security or hybrid syste= ms. * Flawless understanding of `C++` and object-oriented semantics. - Precision-drive our infrastructure: * Technical administration of Linux environments and development tools. * Robust grasp of IT service management processes. - Help us spread the word: * Strong proficiency in foreign languages. * A knack for writing and editing longform content.
=3D=3D Applying =3D=3D If you're interested in joining LSL, send us an email to share what ins= pires you, and why you think you are a good match for the team. Send it wit= h a resume at = florent.kirchner@cea.fr.
[#] http://www-list.cea.fr/index.php/en/technological-research/research-progra= mmes/embedded-systems/validation-and-verification

--
Boris Yakobowski
CEA LIST
--089e0122af2a28c784051e38673d--