[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
*** Please feel free to circulate this message ***
*** Sorry for the multiple receptions ***
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).
*Assignments:*
The purpose of this position is to strengthen the software development
capabilities of the MaREL team (specialized in the field of software
engineering) of the Computer Science department of LIRMM.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.
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.
In more detail, the assignments of the hired person will include:
*
Improving tests for proof search with equality. Equality reasoning
is implemented but further testing is required for validation.
*
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.
*
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.
*
Testing the tool on the whole TPTP problems collection. This library
of problems is used in particular for the CASC competition.
*
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.
*Activities:*
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).
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.
*Skills:*
The candidate must demonstrate the following:
*
High motivation for exploratory work in coordination with researchers
*
Familiarity with the notions of proof and proof search
*
Familiarity with concurrent programming (regardless of the
programming language)
*
Aptitude for collaborative development and version management using Git
*
Experience with Agile project management
*
Excellent aptitude to work in collaboration and to engage external users
*
Fluency in English, both written and oral, for the purpose of
scientific communication
*
Basic knowledge of French, with the intent to learn the language
*
Autonomy and initiative, aptitude to make technical decisions and
justify them in the context of the project
*
Affinity for open-source software development
*Context:*
LIRMM (Laboratoire d'Informatique, de Robotique et de Microélectronique
de Montpellier) is a research department (/unité mixte de recherche/)
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.
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.
The hired person will more specifically join the MaREL team.
*Contact :*
To send your application or simply to have more information about this
position, contact the following people:
*
David Delahaye ([email protected]
<mailto:[email protected]>_).
*
Simon Robillard ([email protected]
<mailto:[email protected]>_).
--
7.5.8 - 27/08/2021
David DELAHAYE
Professor
Head of the Computer Science Departement
Faculty of Sciences
LIRMM UMR 5506
Bt. 4 – CC477 • 161 rue Ada
34095 Montpellier Cedex 5 • France
Phone: +33 (0)4 67 41 86 01 <tel:+33 (0)4 67 41 86 01>
[email protected] <mailto:[email protected]>
https://urldefense.com/v3/__http://www.lirmm.fr/*delahaye/__;fg!!IBzWLUs!Sq5R6Eo4VzKVeT7DWPoeMDo_6DNQIYq46XnCx3kkb206N0_VRQbwbIkBNZ2RWQ4Ra_-A_UlPp2P3i_btw3uECf-oLCD0g84A3GqAzj3X$
<https://urldefense.com/v3/__http://www.umontpellier.fr/__;!!IBzWLUs!Sq5R6Eo4VzKVeT7DWPoeMDo_6DNQIYq46XnCx3kkb206N0_VRQbwbIkBNZ2RWQ4Ra_-A_UlPp2P3i_btw3uECf-oLCD0g84A3Etx4xbo$
>
<https://urldefense.com/v3/__http://http:/*www.lirmm.fr/*delahaye/__;L34!!IBzWLUs!Sq5R6Eo4VzKVeT7DWPoeMDo_6DNQIYq46XnCx3kkb206N0_VRQbwbIkBNZ2RWQ4Ra_-A_UlPp2P3i_btw3uECf-oLCD0g84A3I1eYtMd$
>
UNIVERSITÉ DE MONTPELLIER
Département Informatique
Bt. 16 – CC 12 • Place Eugène Bataillon
34095 Montpellier cedex 05 • France
informatique-fds.edu.umontpellier.fr
<https://urldefense.com/v3/__https://informatique-fds.edu.umontpellier.fr/__;!!IBzWLUs!Sq5R6Eo4VzKVeT7DWPoeMDo_6DNQIYq46XnCx3kkb206N0_VRQbwbIkBNZ2RWQ4Ra_-A_UlPp2P3i_btw3uECf-oLCD0g84A3LILaZ83$ >
<#> <#> <#> <#> <#>
