Positions within the ReacHard Project

The ANR project ReacHard proposes several internships and positions on reachability problems for counter systems, including vector addition systems and related models. The positions can start in 2011 or 2012 and will take place at either LaBRI or at LSV France.

How to Apply

Candidates to positions should hold a Master degree in Computer Science (ideally with courses in formal verification, theoretical computer science and mathematical structures for CS) or equivalently is graduated from a Computer Science Engineering School with a strong background in theoretical computer science.

Applications should be sent to anr-reachard@lsv.ens-cachan.fr. Required documents are:

  • a detailed curriculum vitae
  • a copy of the Master diploma or equivalent
  • a reference letter by their Master supervisor.

The ReacHard Project in a Nutshell

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.

More specifically, 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. Recent breakthroughs on the problem and on related problems for variant models should also allow us to propose solutions for several extensions, including for instance VASS with one stack or branching VASS.

Furthermore, the goal is to take advantage of the new proof techniques involving semilinear separators designed by J. Leroux in order to design algorithms that are amenable for implementation. We propose to develop original techniques in order to solve the following difficult issues:

  • to understand the mathematical structure of reachability sets and relations in vector addition systems,
  • to develop new techniques for the computational analysis of reachability problems that are verification problems connected in some way to the reachability problem for VASS or their extensions,
  • to design algorithms, for instance in the lines of Karp & Miller algorithms, or by relating flattening methods and semilinearity,
  • to widen the scope of our analysis to models richer than VASS, including models with restricted zero-tests or with branching computations.

PhD Subjects

Here are four examples of research subjects that can be pursued in the context of ReacHard:

Master Subjects

We are also seeking students for internships in ReacHard on similar subjects (and leading to PhD theses):

Any further inquiry should be sent to anr-reachard@lsv.ens-cachan.fr.