A Complete Bounded Model Checking Algorithm for Pushdown Systems - Basler, G; Kroening, D; Weissenbacher, G (Springer, 2007)