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