Hiring/BDDPolyhedra

The STATOR project is hiring a PhD student.

Keywords

convex polyhedra; parametric linear programming; binary decision diagrams; satisfiability testing; computer proofs.

Context

Convex polyhedra are powerful approach to representing sets of states of software or of a control system from which that system cannot escape. Such sets of states are used to automatically show that some error conditions are unreachable.

General convex polyhedra were commonly considered too costly to be applied to many variables at once, because of the "curse of dimensionality". The traditional approach to algorithms on convex polyhedra is the double representation (as vertices and faces), which has well-known exponential cases that occur in common cases (e.g. hypercubes). Because of this, they were commonly restricted to low dimensions, or to special subclasses (e.g. products of intervals, "octagons").

At VERIMAG, we have developed an approach for representing polyhedra as constraints only. Our recent progress on efficient approaches to parametric linear programming have shown that it can be used as a very efficient basic block for the algorithms operating over such a representation.

In parallel, sets of vectors of Booleans are commonly represented using binary decision diagrams (BDDs) or similar structures. These are used in model-checking, again for showing that some error conditions are unreachable.

It is very tempting to combine convex polyhedra and Boolean reasoning. Attempts so far (e.g. the BDDApron library) have however had somewhat disappointing performance.

Goals

We are interested in the design of algorithms operating over maps from $\{0,1\}^n$ to the set of convex polyhedra, where commonality between several polyhedra in the same map will be exploited so as to avoid useless duplication of computations.

Working Context

The thesis will be co-advised by Michaël Périn and David Monniaux. The PhD student will be hosted by the Verimag laboratory, near Grenoble in the French Alps. The Grenoble area, in addition to the surrounding mountains known for winter sports, features one of Europe's largest concentrations of academic/industrial research and development with a lot of students and a relatively-cosmopolite atmosphere. You can easily reach Lyon (1 hour), Geneva (1.5 hours), Torino (2 hours), Paris (3 hours by train) and Barcelona (6 hours).

Required Skills

Motivated candidates should hold a Master's degree and have a solid background in \textbf{either} computer science or operation research (linear programming etc.). Good programming skills are also required, in OCaml and/or C++.

Procedure

The candidates are kindly asked to send an e-mail with "PhD candidate" in the title, a CV and motivation letter to Michaël Périn and David Monniaux.

Knowledge of French is not a prerequisite (courses of French language will be covered by the lab).