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 6D2197F89E for ; Fri, 4 Apr 2014 10:13:39 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of julien.signoles@gmail.com) identity=pra; client-ip=209.85.212.180; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="julien.signoles@gmail.com"; x-sender="julien.signoles@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of julien.signoles@gmail.com designates 209.85.212.180 as permitted sender) identity=mailfrom; client-ip=209.85.212.180; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="julien.signoles@gmail.com"; x-sender="julien.signoles@gmail.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-wi0-f180.google.com) identity=helo; client-ip=209.85.212.180; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="julien.signoles@gmail.com"; x-sender="postmaster@mail-wi0-f180.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AicCACxoPlPRVdS0lGdsb2JhbABXhBjEAYEYCBYOAQEBAQcLCwkSKoJsARsPBggBAxIQXQERAQUBIhMUBYdLAQMRoGGMWgWDDpcQChknDWSGQREBBQyJOoRJEQFQhD8EmFuQUBgpgx+BQTuBLgcXBg X-IPAS-Result: AicCACxoPlPRVdS0lGdsb2JhbABXhBjEAYEYCBYOAQEBAQcLCwkSKoJsARsPBggBAxIQXQERAQUBIhMUBYdLAQMRoGGMWgWDDpcQChknDWSGQREBBQyJOoRJEQFQhD8EmFuQUBgpgx+BQTuBLgcXBg X-IronPort-AV: E=Sophos;i="4.97,793,1389740400"; d="scan'208";a="55517794" Received: from mail-wi0-f180.google.com ([209.85.212.180]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 04 Apr 2014 10:13:38 +0200 Received: by mail-wi0-f180.google.com with SMTP id q5so726936wiv.7 for ; Fri, 04 Apr 2014 01:13:38 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:date:message-id:subject:from:to:cc:content-type; bh=HwEIF09VPm1Z9k99vo83JNLWd9gLzUZjDrEH2c/VZkw=; b=PqPa2UJVqpx7COk1b3aRIP6SsPWnjDDnYYzNS4EiAORIL1q3/le+QovtWr3FN4B2bG WQ1tKkqdPS1D6kVbL2pw7ahhRmbaw0gVJ/JcJOk/IaeN0b8ogXzkcxUoeCa/JHzY2BDG x3L9vBGF2I99NWE8jfdSiF0vRZg53GTz/J3Ec6uaHQybA3CS6SkzAQ25R8aAgBQ/wp5M QiN41WtyzP1m/QwP2PRBQ1EnTC44u+iXHf4Aakfy8H3fefOWWJKND3VLgDgeRVNGuD0J uTmLOgwlKwurNT4L/WonHtKscHrCrkco7JJJzdp2sw/Sg+OGCzh3qB0WCKlaZ7XDFtro rJsA== MIME-Version: 1.0 X-Received: by 10.194.82.69 with SMTP id g5mr17546720wjy.85.1396599218318; Fri, 04 Apr 2014 01:13:38 -0700 (PDT) Received: by 10.15.75.9 with HTTP; Fri, 4 Apr 2014 01:13:38 -0700 (PDT) Date: Fri, 4 Apr 2014 10:13:38 +0200 Message-ID: From: Julien Signoles To: Caml List Cc: KIRCHNER Florent Content-Type: multipart/alternative; boundary=047d7bb047944d342804f6331806 Subject: [Caml-list] [JOB] OCaml Engineers and Scientists at CEA, Software Security Labs (Paris Saclay, France) --047d7bb047944d342804f6331806 Content-Type: text/plain; charset=ISO-8859-1 Hi List, The CEA' Software Security Laboratory is opening positions for OCaml engineers and scientists at Paris Saclay, France. ## Engineer & Scientist. ### Research and develop the next-generation of software verification tools. The Software Security Laboratory - LSL - has an ambitious goal: enable developers and validation experts to design high-confidence software. We believe that programs should be as reliable as mathematical truths. Within CEA, LSL is dedicated to inventing the best possible means to conduct software verification. We craft methods and tools that leverage exciting, cutting-edge formal methods to ensure that industrial code can comply with the highest standards. And in doing so, we get to interact with the most creative people in academia and the industry. Our organizational structure is very simple: those who pioneer scientific innovations are the same ones who implement them. We are a dynamic twenty-person laboratory, and your work will have a direct and visible impact on the state of formal verification. Our brand-new offices are located in the heart of Campus Paris Saclay, in the largest European cluster of public and private research. * #### You You dream of devising the next breakthrough in code analysis and to see it through low-level implementation details. You read research papers with passion, but you are fully aware that a toy prototype is quite different from a hardened tool. You understand that what stands between both is a series of complex implementation problems. And that's great, because it means getting your hands dirty and confronting your tools to challenging real-life use cases. 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 the Frama-C platform, by improving the current analyses and designing complementary approaches. You will contribute to growing the community of users, handling feedback and helping real people solve real problems. You will take an active part 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. - Experience with significant OCaml development. - Experience with software engineering practices: source code management and reviews, continuous integration, and bug-tracking. - Self-organized, with an ability to prioritize effectively. - Team-minded - you know when to let someone else take the lead. #### Pluses - Strong proficiency in foreign languages. - Experience with writing scientific papers and technical reports. - Understanding of C or C++ semantics. - Knowledge in the fields of cybersecurity, concurrency, or floating-point arithmetics. - Administration of Linux environments and software development tools. - Design of Graphical User Interfaces. - Hands-on experience with formal verification tools: Coq, PVS, Why3, etc. #### Applying If you're interested in joining LSL, send us an email to share what inspires you, and why you think you are perfect for the team. Send it along with a resume at florent.kirchner@cea.fr. Julien Signoles -- Researcher-engineer CEA LIST, Software Security Labs tel:(+33)1.69.08.00.18 fax:(+33)1.69.08.83.95 Julien.Signoles@cea.fr --047d7bb047944d342804f6331806 Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable
Hi List,

The CEA' Software Security = Laboratory is opening positions for OCaml engineers and scientists at Paris= Saclay, France.

## Engineer & Scientist.
### Resea= rch and develop the next-generation of software verification tools.

The Software Security Laboratory - LSL - has an ambitious goal: enable<= br>developers and validation experts to design high-confidence software. We=
believe that programs should be as reliable as mathematical truths.

Within CEA, LSL is dedicated to inventing the best possible means to co= nduct
software verification. We craft methods and tools that leverage ex= citing,
cutting-edge formal methods to ensure that industrial code can c= omply with the
highest standards. And in doing so, we get to interact with the most creati= ve
people in academia and the industry.

Our organizational struct= ure is very simple: those who pioneer scientific
innovations are the sam= e ones who implement them. We are a dynamic twenty-person
laboratory, and your work will have a direct and visible impact on the stat= e of
formal verification.

Our brand-new offices are located in th= e heart of Campus Paris Saclay, in
the largest European cluster of publi= c and private research.

=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0= =A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0 *


#### You

You dr= eam of devising the next breakthrough in code analysis and to see it
thr= ough low-level implementation details. You read research papers with
passion, but you are fully aware that a toy prototype is quite different fr= om a
hardened tool. You understand that what stands between both is a se= ries of complex
implementation problems. And that's great, because i= t means getting your hands
dirty and confronting your tools to challenging real-life use cases.
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 thi= ng. 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 the Frama-C platform, by improving the c= urrent
analyses and designing complementary approaches. You will contrib= ute to growing the
community of users, handling feedback and helping rea= l people solve real problems.

You will take an active part in research activities and industrial
p= artnerships, alongside other members of the laboratory. This can includewriting proposals, managing projects, publishing papers, and attending
scientific and technical events worldwide.

#### Requirements

= - Background in formal methods, and programming languages.
- Experience = with significant OCaml development.
- Experience with software engineeri= ng practices: source code management and
=A0 reviews, continuous integration, and bug-tracking.
- Self-organized,= with an ability to prioritize effectively.
- Team-minded - you know whe= n to let someone else take the lead.

#### Pluses

- Strong pro= ficiency in foreign languages.
- Experience with writing scientific papers and technical reports.
- Und= erstanding of C or C++ semantics.
- Knowledge in the fields of cybersecu= rity, concurrency, or floating-point
=A0 arithmetics.
- Administratio= n of Linux environments and software development tools.
- Design of Graphical User Interfaces.
- Hands-on experience with formal= verification tools: Coq, PVS, Why3, etc.

#### Applying

If yo= u're interested in joining LSL, send us an email to share what inspires=
you, and why you think you are perfect for the team. Send it along with a r= esume
at florent.kirchner@cea= .fr.

Julien Signoles
--
Researcher-= engineer
CEA LIST, Software Security Labs
tel:(+33)1.69.08.00.18=A0 fax:(+33)1.69= .08.83.95=A0 Julien.Signoles@cea.= fr

--047d7bb047944d342804f6331806--