David Monniaux: /* Required Skills */

2016-06-13T15:22:48Z

Required Skills

David Monniaux at 15:22, 13 June 2016

2016-06-13T15:22:14Z

David Monniaux: Created page with "The STATOR project is hiring a PhD student. ==Keywords== convex polyhedra; parametric linear programming; binary decision diagrams; satisfiability testing; computer proofs...."

2016-06-13T15:20:13Z

Created page with "The STATOR project is hiring a PhD student. ==Keywords== convex polyhedra; parametric linear programming; binary decision diagrams; satisfiability testing; computer proofs...."

New page

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 [http://www-verimag.imag.fr/~perin/ Michaël Périn] and [http://www-verimag.imag.fr/~monniaux David Monniaux].

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

@@ Line 22: / Line 22: @@
 ==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++.
+Motivated candidates should hold a Master's degree and have a solid background in '''either''' computer science or operation research (linear programming etc.). Good programming skills are also required, in OCaml and/or C++.
 ==Procedure==

@@ Line 16: / Line 16: @@
 ==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.
+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==

Hiring/BDDPolyhedra - Revision history

David Monniaux: /* Required Skills */

David Monniaux at 15:22, 13 June 2016

David Monniaux: Created page with "The STATOR project is hiring a PhD student. ==Keywords== convex polyhedra; parametric linear programming; binary decision diagrams; satisfiability testing; computer proofs...."