Taming Hard Reachability Problems
The ReacHard project considers some fundamental algorithmic questions in the automatic verification of counter systems, a simple class of infinite-state computational models that play a prominent role in many areas of computer science. The main question we tackle is the reachability problem for VASS, or equivalently Petri Nets. This problem is central and its decidability, first proved in '82, has been widely used in several fields ranging from automated deduction to communication protocols. However, the reachability problem for VASS has been solved in an incomplete and unsatisfactory way (no implementation is known). The main objective of ReacHard is to propose a satisfactory solution to the reachability problem for VASS, that provides significant improvements both conceptually and computationnally.

Number of scientific articles published: 0

Number of patents filed: 0

Number of product’s innovation: 0

Number of product’s innovation service: 0

Number of projected jobs created: 0

Number of jobs maintained: 0

Number of related companies creation: 0