Few is Just Enough! : Small Model Theorem for Parameterized Verification and Shape Analysis

This doctoral thesis considers the automatic verification of parameterized systems, i.e. systems with an arbitrary number of communicating components, such as mutual exclusion protocols, cache cohe ...