Combining Decision Procedures for Constraint Programming and SMT

Open PhD position (3 years)

We are looking for highly motivated PhD candidates in constraint programming, SMT, and software verification. The work will be conducted as part of SOPRANO project, funded by the the french National Research Agency (ANR).

Contacts: Mathieu Acher (mathieu.acher@irisa.fr), Sebastien Bardin (sebastien.bardin@cea.fr), Arnaud Gotlieb (arnaud@simula.no)

Keywords: constraint programming, SMT, satisfiability modulo theories, solvers, software verification

Context

Modern societies crucially rely on digital infrastructures, and it is becoming clear that high-quality software can be obtained only with the help of proper software verification tools. Today most major verification approaches rely on automatic external solvers. Beyond verification, solvers are also widely employed in numerous application domains for performing complex reasoning tasks. These solvers, however, do not fill the current and future needs for verification: lack of satisfying model generation, lack of reasoning on difficult theories, lack of extensibility for specific or new needs.

Objectives

The work will be performed in the context of SOPRANO [1], a research project involving experts from academia and industry that are developing state-of-the-art constraint solving technology. The major results of the project include scientific, technological, and industrial benefits. The project has the potential to deliver significant breakthroughs in automated constraint solving and program analysis [2, 3]. The PhD thesis aims to prepare the next generation of solvers, thus opening avenues for novel verifications and reasoning. The resulting solvers will be more widely applicable, easier to tune for specific applications, and potentially more efficient. The PhD candidate will design a new framework for the cooperation/combination of solvers, focused on model generation and borrowing principles from Satisfiability Modulo Theories (SMT-solving) [4, 5, 8, 9] and Constraint Programming (CP) [6, 7]. Roughly speaking, we seek to add to SMT the extensibility of CP and its native handling of domains, and to CP the elegant communication interfaces of SMT and its ability to reason over formulas with complex boolean structures (conflict analysis) and quantifiers.

References

Working Environment

The candidate will work at Inria in the DIVERSE team (workplace: Université Rennes 1, Campus de Beaulieu, 35000 Rennes, France) in close collaboration with CEA LIST (Saclay, France). He will be registered as a PhD-student of University of Rennes 1, and co-supervised by Mathieu Acher, from the DIVERSE team, Sébastien Bardin from the CEA LIST and Arnaud Gotlieb from Inria Rennes (Habilitated, currently in temporary leave to SIMULA Research Laboratory, Norway). The contract is for 36 months. The monthly net salary is around 1600 euros (net). The candidate will also be invited to complement his research activity with teaching activities and vacations at University of Rennes 1 if it fits with the project and his own desire. DIVERSE's team is actively involved in European, French and industrial projects and is composed of 8 faculty members, 18 PhD students, 5 postdocs and 4 engineers, so that, the selected candidate will benefit from a joyful and productive working environment.

The PhD is intended to start by September 1st, 2015. Please send your application (PDF) as soon as possible (i.e., deadline: June 15th). Screening of applications starts immediately and continues until the position is filled. Please send CV, PDFs of Master thesis (if any; or draft), recommendation letters.



Please contact Mathieu Acher (mathieu.acher@irisa.fr)

Other jobs at DiverSE