Verifying concurrent systems by approximation

Approximate verification frameworks are an approach to combat the well-known state-space explosion problem. For properties formulated as "no bad state can be reached", an approximate framework can be simply obtained by replacing exact reachability by some over-approximation. These frameworks look for a bad state in this over-approximation. If no bad states are found, the system satisfies the original property; the framework is sound. If a bad state is found, we have an inconclusive result: this bad state might be reachable or not. This permitted incompleteness is a cornerstone of such methods and it is a means to obtain efficiency. In this thesis, we propose three techniques to approximate reachability. The first analyses small subsystems to capture locally provable relationships between component states. The second and third complement the first by capturing some global system invariants. While the second combines component invariants to estimate whether components can cooperate to reach a system state, the third technique detects token mechanisms and deduces token invariants that approximate reachability. Moreover, we show how our approximations can give rise to useful frameworks that check deadlock freedom, static properties -- a class of state-based properties we propose -- and CSP's traces and failures refinement expressions. Our evaluation of these frameworks seems to suggest that they can efficiently prove a large spectrum of properties for a variety of systems. Despite tackling NP-hard problems, our frameworks can be efficiently powered by SAT/SMT solvers. The unsuccessful attempts at using symbolic exploration to precisely check concurrent systems, combined with the success of our frameworks, suggest that the approximations we study are a key factor in harnessing the verification power of these solvers.