PhD student position in reachability problems, Bordeaux (France)

The ANR project REACHARD proposes several PhD positions on reachability problems for counter systems, including vector addition systems and related models. The PhD position can start in 2011 or 2012 and will take place either at LaBRI or at LSV , France. The duration is 3 years, with an annual salary of 21,000 euros after tax + benefits.

The main objective of the ANR project REACHARD is to propose a satisfactory solution to the reachability problem for vector addition systems, that will provide significant improvements both conceptually and computationally. Many standard verification problems can be rephrased as reachability problems, and there exist powerful methods for infinite-state systems; see e.g. the theory of well-structured transition systems. However, obtaining decision procedures is not the ultimate goal, which we rather see in crafting provably optimal algorithms---required for practical use. In the ANR project REACHARD, we focus on algorithmic issues for the verification of counter systems, more specifically to reachability problems for vector addition systems with states (VASS) and related models.

For more information, see http://www.lsv.ens-cachan.fr/Projects/anr-reachard/Documents/Announce. Any further inquiry should be sent to anr-reachard at lsv.ens-cachan.fr.