<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>