The Coq mailing list

[David Delahaye <David.Delahaye AT lirmm.fr>]

*** 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 (David.Delahaye AT lirmm.fr).
* Simon Robillard (Simon.Robillard AT lirmm.fr).