PhD Thesis in CP and SMT-solving at Inria Rennes

Combining Decision Procedures for Constraint Programming and SMT
—
| Position type: PhD Student
—
Functional area: Rennes
Research theme: Networks, systems and services, distributed computing
Project: DIVERSE
Scientific advisor: arnaud.gotlieb@inria.fr
HR Contact: sophie.viaud@inria.fr
Application deadline: 31/12/2015

About Inria

Established in 1967, Inria is the only public research body fully dedicated to computational sciences.
Combining computer sciences with mathematics, Inria’s 3,500 researchers strive to invent the digital technologies of the future. Educated at leading international universities, they creatively integrate basic research with applied research and dedicate themselves to solving real problems, collaborating with the main players in public and private research in France and abroad and transferring the fruits of their work to innovative companies.
The researchers at Inria published over 4,500 articles in 2013. They are behind over 300 active patents and 120 start-ups. The 172 project teams are distributed in eight research centers located throughout France.

Topic

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.

Keywords and references

constraint programming
SMT
satisfiability modulo theories
solvers
software verification

Profil recherché

1. SOPRANO
2. SPARK
3. Frama-C
4. Alt-Ergo: http://alt-ergo.lri.fr/ http://alt-ergo.ocamlpro.com/
5. H. Ganzinger, G. Hagen, R. Nieuwenhuis, A. Oliveras, and C. Tinelli. DPLL(T): fast decision procedures. In R. Alur and D. A. Peled, editors, Computer Aided Verication, number 3114 in LNCS, pages 175{188. Springer Berlin Heidelberg, Jan. 2004.
6. A. Gotlieb. TCAS software verification using constraint programming. The Knowledge Engineering Review, 27(3):343{360, Sep. 2012.
7. S. Bardin and A. Gotlieb. FDCC: a combined approach for solving constraints over nite domains and arrays. In Proc. of Constraint Programming, Artifical Intelligence, Operational Research (CPAIOR’12), May. 2012.
8. F. Bobot, S. Conchon, E. Contejean, M. Iguernelala, A. Mahboubi, A. Mebsout, and G. Melquiond. A Simplex-based extension of Fourier-Motzkin for solving linear integer arithmetic. In IJCAR. 2012.
9. G. Nelson and D. C. Oppen. Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems (TOPLAS), 1(2):245{257, 1979.

Contacts

PhD Supervisor : Arnaud Gotlieb
PhD Advisors :
Mathieu Acher
Sébastien Bardin
Contacts :
mathieu.acher@irisa.fr
arnaud@simula.no

Security and defence procedure

In the interests of protecting its scientific and technological assets, Inria is a restricted-access establishment. Consequently, it follows special regulations for welcoming any person who whishes to work with the institute. The final acceptance of each candidate thus depends on applying this security and defence procedure.