<html>
  <head>

    <meta http-equiv="content-type" content="text/html; charset=UTF-8">
  </head>
  <body>
    <p> </p>
    <p class="western" style="margin-bottom: 0cm; line-height: 100%"
      align="justify">*** Please feel free to circulate this message ***<br>
      *** Sorry for the multiple receptions ***</p>
    <p class="western" style="margin-bottom: 0cm; line-height: 100%"
      align="justify">
      The LIRMM (UMR 5506, University of Montpellier, CNRS) is
      recruiting a full-time research engineer for a period of 12 months
      in the field of automated proof. The desired start date is January
      1, 2023, and the position will be located in Montpellier (France).<br>
    </p>
    <p class="western" style="margin-bottom: 0cm; line-height: 100%"><b>Assignments:</b></p>
    <p class="western" style="margin-bottom: 0cm; line-height: 100%"
      align="justify">
      <span style="font-weight: normal">The purpose of this position is
        to
        strengthen the software development capabilities of the MaREL
        team
      </span><span style="font-weight: normal">(specialized in the field
        of
        software engineering) of the Computer Science department of
        LIRMM.</span><span style="font-weight: normal">
        The person hired will be involved in the development of Goéland,
        an
        automated reasoning tool developed in the team by Julie Cailler
        (PhD
        student) for over a year. This tool is based upon a new proof
        search
        procedure for first-order logic, which leverages concurrency to
        produce proofs in the context of the tableaux method. This tool
        currently gives excellent results (as measured by the number of
        solved problems) in comparison with similar tools. Notably, it
        achieves better results in some problem categories than similar
        (tableaux-based) tools, some of which have been established for
        years. A conference article on Goéland has been accepted for
        publication at IJCAR 2022, a rank A conference, demonstrating
        the
        interest of the community for the approach used by that tool.
        Furthermore, Goéland has taken part in the CASC-J11 competition,
        organized in parallel with IJCAR 2022, and in which the current
        best
        automated deduction tools compete on different sets of problems.
        The
        tool has been awarded the “best newcomer” distinction during
        this
        competition.</span></p>
    <p class="western" style="margin-bottom: 0cm; line-height: 100%"
      align="justify">
      <span style="font-weight: normal">The hired person will
        participate
        in the development and maintenance of the Goéland software,
        which is
        developed using Go, a language suited to concurrent programming.
        The
        aim of this position is twofold. The first mission is to get the
        tool
        in working for competitions, particularly CASC, a yearly
        occurrence
        that serves as a display of our work. The second is to apply the
        tool
        in a more industrial setting. A benchmark of problems
        originating
        from the modeling of industrial applications with the B method
        is
        already available (as a result of the ANR project Bware) but a
        number
        of extensions to Goéland are needed before it can be used on
        this
        benchmark.</span></p>
    <p class="western" style="margin-bottom: 0cm; line-height: 100%"
      align="justify">
      <span style="font-weight: normal">In more detail, the assignments
        of
        the hired person will include:</span></p>
    <ul>
      <li>
        <p class="western" style="margin-bottom: 0cm; line-height: 100%"
          align="justify"> <span style="font-weight: normal">Improving
            tests for proof search with equality. Equality reasoning is
            implemented but further testing is required for validation.</span></p>
      </li>
      <li>
        <p class="western" style="margin-bottom: 0cm; line-height: 100%"
          align="justify"> <span style="font-weight: normal">Integrating
            polymorphism in the proof search. Proof search with
            polymorphic types has been developed recently, but this
            feature has yet to be integrated and also requires tests for
            validation.</span></p>
      </li>
      <li>
        <p class="western" style="margin-bottom: 0cm; line-height: 100%"
          align="justify"> <span style="font-weight: normal">Integrating
            linear arithmetic reasoning in the proof search. Currently,
            the simplex method (for problems involving rational numbers)
            and the branch and cut algorithm (for problems involving
            integers) have been developed but their integration and
            testing remain to be done.</span></p>
      </li>
      <li>
        <p class="western" style="margin-bottom: 0cm; line-height: 100%"
          align="justify"> <span style="font-weight: normal">Testing
            the tool on the whole TPTP problems collection. This library
            of problems is used in particular for the CASC competition.</span></p>
      </li>
      <li>
        <p class="western" style="margin-bottom: 0cm; line-height: 100%"
          align="justify"> <span style="font-weight: normal">Testing
            the tool on the benchmark of industrial problems taken from
            the ANR project BWare . This test can only be carried out
            after the integration of polymorphism and linear reasoning
            in the tool.</span></p>
      </li>
    </ul>
    <p class="western" style="margin-bottom: 0cm; line-height: 100%"
      align="justify">
      <span lang="en-US"><b>Activities:</b></span></p>
    <p class="western" style="margin-bottom: 0cm; line-height: 100%"
      align="justify">
      <span lang="en-US"><span style="font-weight: normal">The hired
          person
          will work under the direction of David Delahaye (PR/full
          professor in
          the team MaREL), Simon Robillard (MCF/associate professor in
          the team
          MaREL), and Julie Cailler (PhD student in the team MaREL, with
          a
          thesis on the topic, and the main developer of Goéland).</span></span></p>
    <p class="western" style="margin-bottom: 0cm; line-height: 100%"
      align="justify">
      <span lang="en-US"><span style="font-weight: normal">The technical
          program follows the assignments described in the previous
          section.
          The order of assignments is not critical, with the exception
          of tests
          on the BWare benchmarks, for which the integration of
          polymorphism
          and linear arithmetic reasoning are prerequisites.</span></span></p>
    <p class="western" style="margin-bottom: 0cm; line-height: 100%"
      align="justify">
      <span lang="en-US"><b>Skills:</b></span></p>
    <p class="western" style="margin-bottom: 0cm; line-height: 100%"
      align="justify">
      <span lang="en-US"><span style="font-weight: normal">The candidate
          must demonstrate the following:</span></span></p>
    <ul>
      <li>
        <p class="western" style="margin-bottom: 0cm; line-height: 100%"
          align="justify"> <span lang="en-US"><span style="font-weight:
              normal">High motivation for exploratory work in
              coordination with researchers</span></span></p>
      </li>
      <li>
        <p class="western" style="margin-bottom: 0cm; line-height: 100%"
          align="justify"> <span lang="en-US"><span style="font-weight:
              normal">Familiarity with the notions of proof and proof
              search</span></span></p>
      </li>
      <li>
        <p class="western" style="margin-bottom: 0cm; line-height: 100%"
          align="justify"> <span lang="en-US"><span style="font-weight:
              normal">Familiarity with concurrent programming
              (regardless of the programming language)</span></span></p>
      </li>
      <li>
        <p class="western" style="margin-bottom: 0cm; line-height: 100%"
          align="justify"> <span lang="en-US"><span style="font-weight:
              normal">Aptitude for collaborative development and version
              management using Git</span></span></p>
      </li>
      <li>
        <p class="western" style="margin-bottom: 0cm; line-height: 100%"
          align="justify"> <span lang="en-US"><span style="font-weight:
              normal">Experience with Agile project management</span></span></p>
      </li>
      <li>
        <p class="western" style="margin-bottom: 0cm; line-height: 100%"
          align="justify"> <span lang="en-US"><span style="font-weight:
              normal">Excellent aptitude to work in collaboration and to
              engage external users</span></span></p>
      </li>
      <li>
        <p class="western" style="margin-bottom: 0cm; line-height: 100%"
          align="justify"> <span lang="en-US"><span style="font-weight:
              normal">Fluency in English, both written and oral, for the
              purpose of scientific communication</span></span></p>
      </li>
      <li>
        <p class="western" style="margin-bottom: 0cm; line-height: 100%"
          align="justify"> <span lang="en-US"><span style="font-weight:
              normal">Basic knowledge of French, with the intent to
              learn the language</span></span></p>
      </li>
      <li>
        <p class="western" style="margin-bottom: 0cm; line-height: 100%"
          align="justify"> <span lang="en-US"><span style="font-weight:
              normal">Autonomy and initiative, aptitude to make
              technical decisions and justify them in the context of the
              project</span></span></p>
      </li>
      <li>
        <p class="western" style="margin-bottom: 0cm; line-height: 100%"
          align="justify"> <span lang="en-US"><span style="font-weight:
              normal">Affinity for open-source software development</span></span></p>
      </li>
    </ul>
    <p class="western" style="margin-bottom: 0cm; line-height: 100%"
      align="justify">
      <span lang="en-US"><b>Context:</b></span></p>
    <p class="western" style="margin-bottom: 0cm; line-height: 100%"
      align="justify">
      <span lang="en-US"><span style="font-weight: normal">LIRMM
          (Laboratoire d'Informatique, de Robotique et de
          Microélectronique de
          Montpellier) is a research department (</span></span><span
        lang="en-US"><i><span style="font-weight: normal">unité
            mixte de recherche</span></i></span><span lang="en-US"><span
          style="font-weight: normal">)
          headed by CNRS and the University of Montpellier. It hosts 410
          employees, including 192 permanent positions. It is organized
          in
          three divisions: Computer Science, Robotics and
          Micro-Electronics, as
          well as centralized services, among which the Research Support
          Service (SAR, comprising 16 engineers) that provides technical
          support for research projects and manages the technology
          platforms of
          the department. The hired engineer will join this service and
          provide
          support for researchers in the department.</span></span></p>
    <p class="western" style="margin-bottom: 0cm; line-height: 100%"
      align="justify">
      <span lang="en-US"><span style="font-weight: normal">The research
          topics of the Computer Science division cover a large spectrum
          ranging from the foundations of computer science (algorithms,
          computation, data science, software engineering, AI) to
          inter-disciplinary research (environment, health, biology).
          This
          division hosts 106 permanent positions (researchers,
          teacher-researchers and engineers) and 71 PhD students in 15
          teams.</span></span></p>
    <p class="western" style="margin-bottom: 0cm; line-height: 100%"
      align="justify">
      <span lang="en-US"><span style="font-weight: normal">The hired
          person
          will more specifically join the MaREL </span></span><span
        lang="en-US"><span style="font-weight: normal">team</span></span><span
        lang="en-US"><span style="font-weight: normal">.</span></span></p>
    <p class="western" style="margin-bottom: 0cm; line-height: 100%"><font
        face="Arial, serif"><b>Contact
          :</b></font></p>
    <p class="western" style="margin-bottom: 0cm; line-height: 100%"
      align="justify">
      To send your application or simply to have more information about
      this position, contact the following people:</p>
    <ul>
      <li>
        <p class="western" style="margin-bottom: 0cm; line-height: 100%">
          <span style="font-weight: normal">David Delahaye (</span><font
            color="#0000ff"><u><a href="mailto:David.Delahaye@lirmm.fr"><span
                  style="font-weight: normal">David.Delahaye@lirmm.fr</span></a></u></font><span
            style="font-weight: normal">).</span></p>
      </li>
      <li>
        <p class="western" style="margin-bottom: 0cm; line-height: 100%">
          <span style="font-weight: normal">Simon Robillard (</span><font
            color="#0000ff"><u><a href="mailto:Simon.Robillard@lirmm.fr"><span
                  style="font-weight: normal">Simon.Robillard@lirmm.fr</span></a></u></font><span
            style="font-weight: normal">).</span></p>
      </li>
    </ul>
    <p>
      <style type="text/css">
                p { margin-bottom: 0.25cm; direction: ltr; color: #00000a; line-height: 120%; text-align: left; orphans: 2; widows: 2 }
                p.western { font-family: "Arial", serif; font-size: 11pt; so-language: en-US }
                p.cjk { font-family: "Arial"; font-size: 11pt; so-language: en-US }
                p.ctl { font-family: "Arial"; font-size: 11pt; so-language: ar-SA }
                a:link { color: #0000ff }</style></p>
    <div class="moz-signature">-- <br>
      <meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
      <div>
        <div style="display:none;"> 7.5.8 - 27/08/2021 </div>
      </div>
      <table id="previsu" style="width: 500px; height: 200px; padding:
        10px; background-color: transparent;" cellspacing="0"
        cellpadding="0" border="0">
        <tbody>
          <tr>
            <td id="donnees" colspan="3" style="vertical-align: top;
              padding-bottom: 10px; border-bottom: 2px dotted rgba(0, 0,
              0, 0.16); border-top: medium none;">
              <p id="pnomcomplet" style="margin: 0px; padding: 0px;
                line-height: 1.4;"><span id="pprenom" style="margin:
                  0px; padding: 0px; text-decoration: none; color:
                  black; font-family: "Arial", sans-serif;
                  font-size: 13px; font-weight: bold; font-style:
                  normal; line-height: 1.4; text-transform: uppercase;">David</span> <span
                  id="pnom" style="margin: 0px; padding: 0px;
                  text-decoration: none; color: black; font-family:
                  "Arial", sans-serif; font-size: 13px;
                  font-weight: bold; font-style: normal; line-height:
                  1.4; text-transform: uppercase;">DELAHAYE</span></p>
              <p style="margin-bottom:-0.3cm"> </p>
              <p id="ptitre" style="margin: 0px; padding: 0px;
                line-height: 1.2; text-decoration: none; color: rgb(0,
                43, 81); font-family: "Arial", sans-serif;
                font-size: 13px; font-weight: bold; font-style: normal;
                text-transform: uppercase;">Professor</p>
              <p id="pinfos" style="display: block; font-weight: 300;
                margin: 0px; padding: 0px; text-decoration: none; color:
                rgb(0, 43, 81); font-family: "Arial",
                sans-serif; font-size: 13px; font-style: normal;
                line-height: 1;">Head of the Computer Science
                Departement<br>
                Faculty of Sciences</p>
              <p style="margin-bottom:-0.2cm"> </p>
              <p id="ppostale" style="margin: 0px; padding: 0px;
                line-height: 1.2; font-weight: normal; font-size: 13px;"><span
                  id="pcasecourier" style="margin: 0px; padding: 0px;
                  text-decoration: none; color: black; font-family:
                  "Arial", sans-serif; font-size: 13px;
                  font-weight: normal; font-style: normal; line-height:
                  1.2;">LIRMM UMR 5506<br>
                  Bt. 4 – CC477 • 161 rue Ada<br>
                  34095 Montpellier Cedex 5 • France</span><span
                  id="padresse" style="margin: 0px; padding: 0px;
                  text-decoration: none; color: black; font-family:
                  "Arial", sans-serif; font-size: 13px;
                  font-weight: normal; font-style: normal; line-height:
                  1.2;"></span></p>
              <p id="pnumeros" style="margin: 0px; padding: 0px;
                text-decoration: none; color: black; font-family:
                "Arial", sans-serif; font-size: 13px;
                font-weight: 300; font-style: normal; line-height: 1.2;"><span
                  id="ptellabel" style="font-weight: normal; font-size:
                  13px;">Phone: </span><a href="tel:+33 (0)4 67 41 86
                  01" title="tel:+33 (0)4 67 41 86 01"
                  style="text-decoration: none; margin: 0px; padding:
                  0px; color: black; font-family: "Arial",
                  sans-serif; font-size: 13px; font-weight: 300;
                  font-style: normal; line-height: 1.2;"><span id="ptel">+33
                    (0)4 67 41 86 01</span></a></p>
              <p id="pemail" style="margin: 0px; padding: 0px;
                line-height: 1.2; text-decoration: none; color: black;
                font-family: "Arial", sans-serif; font-size:
                13px; font-weight: 300; font-style: normal;"><a
                  href="mailto:David.Delahaye@lirmm.fr"
                  title="mailto:David.Delahaye@lirmm.fr" style="margin:
                  0px; padding: 0px; text-decoration: none; color:
                  black; font-family: "Arial", sans-serif;
                  font-size: 13px; font-weight: 300; font-style: normal;
                  line-height: 1.2;">David.Delahaye@lirmm.fr</a></p>
              <p id="pweb" style="margin: 0px; padding: 0px;
                line-height: 1.2; text-decoration: none; color: black;
                font-family: "Arial", sans-serif; font-size:
                13px; font-weight: 300; font-style: normal;"><a href="https://urldefense.com/v3/__http://www.lirmm.fr/*delahaye/__;fg!!IBzWLUs!Sq5R6Eo4VzKVeT7DWPoeMDo_6DNQIYq46XnCx3kkb206N0_VRQbwbIkBNZ2RWQ4Ra_-A_UlPp2P3i_btw3uECf-oLCD0g84A3GqAzj3X$" title="http://www.lirmm.fr/~delahaye/" style="margin:
                  0px; padding: 0px; text-decoration: none; color:
                  black; font-family: "Arial", sans-serif;
                  font-size: 13px; font-weight: 300; font-style: normal;
                  line-height: 1.2;">http://www.lirmm.fr/~delahaye/</a></p>
            </td>
          </tr>
          <tr>
            <td colspan="3" style="height: 10px;"><br>
            </td>
          </tr>
          <tr>
            <td id="logo-universite"
              style="height:90px;width:95px;text-align: center;
              vertical-align: center; padding-top: 0px; padding-right:
              25px; width: 1%;"><a id="logo-universite" href="https://urldefense.com/v3/__http://www.umontpellier.fr/__;!!IBzWLUs!Sq5R6Eo4VzKVeT7DWPoeMDo_6DNQIYq46XnCx3kkb206N0_VRQbwbIkBNZ2RWQ4Ra_-A_UlPp2P3i_btw3uECf-oLCD0g84A3Etx4xbo$" title=""><img
                  src="cid:part6.E1482D7A.DB92F86B@lirmm.fr" alt=""
                  style="border: 0px !important;"></a></td>
            <td id="logo-composante" style="border-left: 2px dotted
              rgba(0, 0, 0, 0.16);padding-left:25px;text-align: center;
              vertical-align: center; padding-top: 0px; padding-right:
              0px; width: 1%;"><a id="logo-composante" href="https://urldefense.com/v3/__http://http:/*www.lirmm.fr/*delahaye/__;L34!!IBzWLUs!Sq5R6Eo4VzKVeT7DWPoeMDo_6DNQIYq46XnCx3kkb206N0_VRQbwbIkBNZ2RWQ4Ra_-A_UlPp2P3i_btw3uECf-oLCD0g84A3I1eYtMd$" title="http://http://www.lirmm.fr/~delahaye/"><img
                  src="cid:part8.18BDA2B9.EAB03CDC@lirmm.fr" alt=""
                  style="border: 0px !important;"></a></td>
            <td id="donnees-2" style="padding: 0px 0 0 20px;">
              <p id="petablissement" style="margin: 0px; padding: 0px;
                line-height: 1.2;"><span id="pcomposante" style="margin:
                  0px; padding: 0px; text-decoration: none; color:
                  black; font-family: "Arial", sans-serif;
                  font-size: 13px; font-weight: 300; font-style: normal;
                  line-height: 1.2; text-transform: uppercase;">UNIVERSITÉ
                  DE MONTPELLIER</span></p>
              <p id="ppostale" style="margin: 0px; padding: 0px;
                line-height: 1.2; font-weight: normal; font-size: 13px;"><span
                  id="pcasecourier" style="margin: 0px; padding: 0px;
                  text-decoration: none; color: black; font-family:
                  "Arial", sans-serif; font-size: 13px;
                  font-weight: normal; font-style: normal; line-height:
                  1.2;">Département Informatique<br>
                  Bt. 16 – CC 12 • Place Eugène Bataillon<br>
                </span><span id="padresse" style="margin: 0px; padding:
                  0px; text-decoration: none; color: black; font-family:
                  "Arial", sans-serif; font-size: 13px;
                  font-weight: normal; font-style: normal; line-height:
                  1.2;">34095 Montpellier cedex 05 • France</span></p>
              <p style="margin-bottom:-0.2cm"> </p>
              <p id="pweb" style="margin: 0px; padding: 0px;
                line-height: 2;"><a href="https://urldefense.com/v3/__https://informatique-fds.edu.umontpellier.fr/__;!!IBzWLUs!Sq5R6Eo4VzKVeT7DWPoeMDo_6DNQIYq46XnCx3kkb206N0_VRQbwbIkBNZ2RWQ4Ra_-A_UlPp2P3i_btw3uECf-oLCD0g84A3LILaZ83$" title="https://informatique-fds.edu.umontpellier.fr/" style="margin: 0px; padding: 0px; text-decoration:
                  none; color: rgb(0, 43, 81); font-family:
                  "Arial", sans-serif; font-size: 10px;
                  font-weight: 800; font-style: normal; line-height:
                  1.2; text-transform: uppercase;">informatique-fds.edu.umontpellier.fr</a></p>
              <p id="rsoc" style="margin: 0px; padding: 0px;
                line-height: 1.2;"> <a id="prsoc_t" href="#"
                  style="display: none;"><img src="#"
                    style="height:30px;"></a> <a id="prsoc_f" href="#"
                  style="display: none;"><img src="#"
                    style="height:30px;"></a> <a id="prsoc_y" href="#"
                  style="display: none;"><img src="#"
                    style="height:30px;"></a> <a id="prsoc_i" href="#"
                  style="display: none;"><img src="#"
                    style="height:30px;"></a> <a id="prsoc_l" href="#"
                  style="display: none;"><img src="#"
                    style="height:30px;"></a> </p>
            </td>
          </tr>
        </tbody>
      </table>
    </div>
  </body>
</html>