We introduce a block-structured programming language which supports object creation, global variables, static scope and recursive procedures with local variables. Because of the combination of recursion, local variables and object creation, the behavior of the program is determined by infinitely many different states. However, we show that a program can be viewed as a type of pushdown automata, for which the halting problem as well as LTL and CTL model checking are decidable.