Saturation algorithms for model-checking pushdown systems

We present a survey of the saturation method for model-checking pushdown systems.